YES 7.676 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule FiniteMap
  ((elemFM :: (Ord b, Ord c) => (c,b)  ->  FiniteMap (c,b) a  ->  Bool) :: (Ord b, Ord c) => (c,b)  ->  FiniteMap (c,b) a  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord b => b  ->  FiniteMap b a  ->  Bool
elemFM key fm = 
case lookupFM fm key of
  Nothing-> False
  Just elt-> True

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm = foldFM (\key elt rest ->(key,elt) : rest) [] fm

  foldFM :: (b  ->  a  ->  c  ->  c)  ->  c  ->  FiniteMap b a  ->  c
foldFM k z EmptyFM = z
foldFM k z (Branch key elt _ fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt _ fm_l fm_r) key_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\keyeltrest→(key,elt) : rest

is transformed to
fmToList0 key elt rest = (key,elt) : rest



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule FiniteMap
  ((elemFM :: (Ord c, Ord b) => (b,c)  ->  FiniteMap (b,c) a  ->  Bool) :: (Ord b, Ord c) => (b,c)  ->  FiniteMap (b,c) a  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord b => b  ->  FiniteMap b a  ->  Bool
elemFM key fm = 
case lookupFM fm key of
  Nothing-> False
  Just elt-> True

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (c  ->  a  ->  b  ->  b)  ->  b  ->  FiniteMap c a  ->  b
foldFM k z EmptyFM = z
foldFM k z (Branch key elt _ fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt _ fm_l fm_r) key_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Case Reductions:
The following Case expression
case lookupFM fm key of
 Nothing → False
 Just elt → True

is transformed to
elemFM0 Nothing = False
elemFM0 (Just elt) = True

The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR

mainModule FiniteMap
  ((elemFM :: (Ord a, Ord b) => (b,a)  ->  FiniteMap (b,a) c  ->  Bool) :: (Ord b, Ord a) => (b,a)  ->  FiniteMap (b,a) c  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord a => a  ->  FiniteMap a b  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (a  ->  c  ->  b  ->  b)  ->  b  ->  FiniteMap a c  ->  b
foldFM k z EmptyFM = z
foldFM k z (Branch key elt _ fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt _ fm_l fm_r) key_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR

mainModule FiniteMap
  ((elemFM :: (Ord c, Ord a) => (a,c)  ->  FiniteMap (a,c) b  ->  Bool) :: (Ord c, Ord a) => (a,c)  ->  FiniteMap (a,c) b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord a => a  ->  FiniteMap a b  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (c  ->  a  ->  b  ->  b)  ->  b  ->  FiniteMap c a  ->  b
foldFM k z EmptyFM = z
foldFM k z (Branch key elt _ fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt _ fm_l fm_r) key_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR

mainModule FiniteMap
  ((elemFM :: (Ord a, Ord c) => (a,c)  ->  FiniteMap (a,c) b  ->  Bool) :: (Ord a, Ord c) => (a,c)  ->  FiniteMap (a,c) b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord a => a  ->  FiniteMap a b  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (c  ->  b  ->  a  ->  a)  ->  a  ->  FiniteMap c b  ->  a
foldFM k z EmptyFM = z
foldFM k z (Branch key elt vw fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt vx fm_l fm_r) key_to_find 
 | key_to_find < key = 
lookupFM fm_l key_to_find
 | key_to_find > key = 
lookupFM fm_r key_to_find
 | otherwise = 
Just elt

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch vy vz size wu wv) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Cond Reductions:
The following Function with conditions
lookupFM EmptyFM key = Nothing
lookupFM (Branch key elt vx fm_l fm_r) key_to_find
 | key_to_find < key
 = lookupFM fm_l key_to_find
 | key_to_find > key
 = lookupFM fm_r key_to_find
 | otherwise
 = Just elt

is transformed to
lookupFM EmptyFM key = lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

lookupFM0 key elt vx fm_l fm_r key_to_find True = Just elt

lookupFM1 key elt vx fm_l fm_r key_to_find True = lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False = lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

lookupFM2 key elt vx fm_l fm_r key_to_find True = lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False = lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find = lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

lookupFM4 EmptyFM key = Nothing
lookupFM4 vvu vvv = lookupFM3 vvu vvv

The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare0 x y True = GT

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare3 x y = compare2 x y (x == y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz

gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vww vwx = gcd3 vww vwx
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz
gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

gcd1 True vww vwx = error []
gcd1 vwy vwz vxu = gcd0 vwz vxu

gcd2 True vww vwx = gcd1 (vwx == 0) vww vwx
gcd2 vxv vxw vxx = gcd0 vxw vxx

gcd3 vww vwx = gcd2 (vww == 0) vww vwx
gcd3 vxy vxz = gcd0 vxy vxz

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal0 x True = `negate` x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed

mainModule FiniteMap
  ((elemFM :: (Ord a, Ord c) => (c,a)  ->  FiniteMap (c,a) b  ->  Bool) :: (Ord a, Ord c) => (c,a)  ->  FiniteMap (c,a) b  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord b => b  ->  FiniteMap b a  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap b a  ->  [(b,a)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (a  ->  b  ->  c  ->  c)  ->  c  ->  FiniteMap a b  ->  c
foldFM k z EmptyFM = z
foldFM k z (Branch key elt vw fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key = lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True = Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True = lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False = lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True = lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False = lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find = lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key = Nothing
lookupFM4 vvu vvv = lookupFM3 vvu vvv

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch vy vz size wu wv) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2Reduce1 vyu vyv x y True = error []
reduce2Reduce1 vyu vyv x y False = reduce2Reduce0 vyu vyv x y otherwise

reduce2D vyu vyv = gcd vyu vyv

reduce2Reduce0 vyu vyv x y True = x `quot` reduce2D vyu vyv :% (y `quot` reduce2D vyu vyv)

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x vvw = gcd'2 x vvw
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vvw = x
gcd'1 vvx vvy vvz = gcd'0 vvy vvz
gcd'2 x vvw = gcd'1 (vvw == 0) x vvw
gcd'2 vwu vwv = gcd'0 vwu vwv

are unpacked to the following functions on top level
gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd' x vvw = gcd0Gcd'2 x vvw
gcd0Gcd' x y = gcd0Gcd'0 x y

gcd0Gcd'1 True x vvw = x
gcd0Gcd'1 vvx vvy vvz = gcd0Gcd'0 vvy vvz

gcd0Gcd'2 x vvw = gcd0Gcd'1 (vvw == 0) x vvw
gcd0Gcd'2 vwu vwv = gcd0Gcd'0 vwu vwv



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed

mainModule FiniteMap
  ((elemFM :: (Ord b, Ord a) => (a,b)  ->  FiniteMap (a,b) c  ->  Bool) :: (Ord b, Ord a) => (a,b)  ->  FiniteMap (a,b) c  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord a => a  ->  FiniteMap a b  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (c  ->  b  ->  a  ->  a)  ->  a  ->  FiniteMap c b  ->  a
foldFM k z EmptyFM = z
foldFM k z (Branch key elt vw fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord b => FiniteMap b a  ->  b  ->  Maybe a
lookupFM EmptyFM key = lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True = Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True = lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False = lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True = lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False = lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find = lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key = Nothing
lookupFM4 vvu vvv = lookupFM3 vvu vvv

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch vy vz size wu wv) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow

mainModule FiniteMap
  (elemFM :: (Ord a, Ord b) => (a,b)  ->  FiniteMap (a,b) c  ->  Bool)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
   
(==) fm_1 fm_2 = sizeFM fm_1 == sizeFM fm_2 && fmToList fm_1 == fmToList fm_2

  elemFM :: Ord b => b  ->  FiniteMap b a  ->  Bool
elemFM key fm = elemFM0 (lookupFM fm key)

  
elemFM0 Nothing = False
elemFM0 (Just elt) = True

  fmToList :: FiniteMap a b  ->  [(a,b)]
fmToList fm = foldFM fmToList0 [] fm

  
fmToList0 key elt rest = (key,elt) : rest

  foldFM :: (b  ->  a  ->  c  ->  c)  ->  c  ->  FiniteMap b a  ->  c
foldFM k z EmptyFM = z
foldFM k z (Branch key elt vw fm_l fm_r) = foldFM k (k key elt (foldFM k z fm_r)) fm_l

  lookupFM :: Ord a => FiniteMap a b  ->  a  ->  Maybe b
lookupFM EmptyFM key = lookupFM4 EmptyFM key
lookupFM (Branch key elt vx fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find

  
lookupFM0 key elt vx fm_l fm_r key_to_find True = Just elt

  
lookupFM1 key elt vx fm_l fm_r key_to_find True = lookupFM fm_r key_to_find
lookupFM1 key elt vx fm_l fm_r key_to_find False = lookupFM0 key elt vx fm_l fm_r key_to_find otherwise

  
lookupFM2 key elt vx fm_l fm_r key_to_find True = lookupFM fm_l key_to_find
lookupFM2 key elt vx fm_l fm_r key_to_find False = lookupFM1 key elt vx fm_l fm_r key_to_find (key_to_find > key)

  
lookupFM3 (Branch key elt vx fm_l fm_r) key_to_find = lookupFM2 key elt vx fm_l fm_r key_to_find (key_to_find < key)

  
lookupFM4 EmptyFM key = Nothing
lookupFM4 vvu vvv = lookupFM3 vvu vvv

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = Pos Zero
sizeFM (Branch vy vz size wu wv) = size


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat(vyw43000, vyw45000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vyw7700), Succ(vyw4000000)) → new_primPlusNat(vyw7700, vyw4000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vyw30000), Succ(vyw400000)) → new_primMulNat(vyw30000, Succ(vyw400000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vyw3000), Succ(vyw40000)) → new_primEqNat(vyw3000, vyw40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs3(Just(vyw300), Just(vyw4000), app(app(ty_@2, bdc), bdd)) → new_esEs0(vyw300, vyw4000, bdc, bdd)
new_esEs2(Left(vyw300), Left(vyw4000), app(ty_[], baf), bag) → new_esEs(vyw300, vyw4000, baf)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), app(app(ty_@2, ba), bb)) → new_esEs0(vyw300, vyw4000, ba, bb)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, app(app(app(ty_@3, gg), gh), ha), fa) → new_esEs1(vyw301, vyw4001, gg, gh, ha)
new_esEs2(Right(vyw300), Right(vyw4000), bbh, app(ty_[], bca)) → new_esEs(vyw300, vyw4000, bca)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, eh, app(app(ty_Either, bac), bad)) → new_esEs2(vyw302, vyw4002, bac, bad)
new_esEs2(Left(vyw300), Left(vyw4000), app(app(ty_@2, bah), bba), bag) → new_esEs0(vyw300, vyw4000, bah, bba)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), app(app(ty_Either, fh), ga), eh, fa) → new_esEs2(vyw300, vyw4000, fh, ga)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), app(app(ty_Either, db), dc), cc) → new_esEs2(vyw300, vyw4000, db, dc)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, app(ty_Maybe, hd), fa) → new_esEs3(vyw301, vyw4001, hd)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), de, app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(vyw301, vyw4001, ea, eb, ec)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, eh, app(app(app(ty_@3, hh), baa), bab)) → new_esEs1(vyw302, vyw4002, hh, baa, bab)
new_esEs2(Left(vyw300), Left(vyw4000), app(app(ty_Either, bbe), bbf), bag) → new_esEs2(vyw300, vyw4000, bbe, bbf)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, eh, app(app(ty_@2, hf), hg)) → new_esEs0(vyw302, vyw4002, hf, hg)
new_esEs3(Just(vyw300), Just(vyw4000), app(app(ty_Either, bdh), bea)) → new_esEs2(vyw300, vyw4000, bdh, bea)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, app(app(ty_Either, hb), hc), fa) → new_esEs2(vyw301, vyw4001, hb, hc)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), app(app(ty_@2, fb), fc), eh, fa) → new_esEs0(vyw300, vyw4000, fb, fc)
new_esEs2(Right(vyw300), Right(vyw4000), bbh, app(app(ty_@2, bcb), bcc)) → new_esEs0(vyw300, vyw4000, bcb, bcc)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), de, app(ty_[], df)) → new_esEs(vyw301, vyw4001, df)
new_esEs2(Right(vyw300), Right(vyw4000), bbh, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs1(vyw300, vyw4000, bcd, bce, bcf)
new_esEs3(Just(vyw300), Just(vyw4000), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs1(vyw300, vyw4000, bde, bdf, bdg)
new_esEs3(Just(vyw300), Just(vyw4000), app(ty_[], bdb)) → new_esEs(vyw300, vyw4000, bdb)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), app(app(app(ty_@3, fd), ff), fg), eh, fa) → new_esEs1(vyw300, vyw4000, fd, ff, fg)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), ca) → new_esEs(vyw301, vyw4001, ca)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, eh, app(ty_Maybe, bae)) → new_esEs3(vyw302, vyw4002, bae)
new_esEs2(Left(vyw300), Left(vyw4000), app(app(app(ty_@3, bbb), bbc), bbd), bag) → new_esEs1(vyw300, vyw4000, bbb, bbc, bbd)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), app(app(app(ty_@3, bc), bd), be)) → new_esEs1(vyw300, vyw4000, bc, bd, be)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), de, app(ty_Maybe, ef)) → new_esEs3(vyw301, vyw4001, ef)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), app(app(ty_Either, bf), bg)) → new_esEs2(vyw300, vyw4000, bf, bg)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), de, app(app(ty_Either, ed), ee)) → new_esEs2(vyw301, vyw4001, ed, ee)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), app(ty_Maybe, gb), eh, fa) → new_esEs3(vyw300, vyw4000, gb)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), app(ty_Maybe, dd), cc) → new_esEs3(vyw300, vyw4000, dd)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), app(ty_[], eg), eh, fa) → new_esEs(vyw300, vyw4000, eg)
new_esEs2(Right(vyw300), Right(vyw4000), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(vyw300, vyw4000, bcg, bch)
new_esEs3(Just(vyw300), Just(vyw4000), app(ty_Maybe, beb)) → new_esEs3(vyw300, vyw4000, beb)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), app(ty_Maybe, bh)) → new_esEs3(vyw300, vyw4000, bh)
new_esEs2(Right(vyw300), Right(vyw4000), bbh, app(ty_Maybe, bda)) → new_esEs3(vyw300, vyw4000, bda)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), app(app(ty_@2, cd), ce), cc) → new_esEs0(vyw300, vyw4000, cd, ce)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), app(ty_[], cb), cc) → new_esEs(vyw300, vyw4000, cb)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), app(app(app(ty_@3, cf), cg), da), cc) → new_esEs1(vyw300, vyw4000, cf, cg, da)
new_esEs2(Left(vyw300), Left(vyw4000), app(ty_Maybe, bbg), bag) → new_esEs3(vyw300, vyw4000, bbg)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, app(app(ty_@2, ge), gf), fa) → new_esEs0(vyw301, vyw4001, ge, gf)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, eh, app(ty_[], he)) → new_esEs(vyw302, vyw4002, he)
new_esEs0(@2(vyw300, vyw301), @2(vyw4000, vyw4001), de, app(app(ty_@2, dg), dh)) → new_esEs0(vyw301, vyw4001, dg, dh)
new_esEs1(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), gc, app(ty_[], gd), fa) → new_esEs(vyw301, vyw4001, gd)
new_esEs(:(vyw300, vyw301), :(vyw4000, vyw4001), app(ty_[], h)) → new_esEs(vyw300, vyw4000, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(ty_@2, bcf), bcg), bcb) → new_lt2(vyw4310, vyw4510, bcf, bcg)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(ty_[], bch), bcb) → new_lt3(vyw4310, vyw4510, bch)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, app(app(ty_@2, bcf), bcg)), bcb)) → new_lt2(vyw4310, vyw4510, bcf, bcg)
new_compare20(vyw430, vyw450, False, bed, bee, bef) → new_ltEs(vyw430, vyw450, bed, bee, bef)
new_compare23(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bfd, app(app(ty_Either, app(app(ty_@2, fg), fh)), fb)) → new_ltEs2(vyw4310, vyw4510, fg, fh)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), app(app(ty_Either, cg), da)), cf)) → new_lt0(vyw4311, vyw4511, cg, da)
new_compare23(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bfd, app(app(ty_Either, app(app(ty_Either, fc), fd)), fb)) → new_ltEs0(vyw4310, vyw4510, fc, fd)
new_compare23(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(app(ty_@3, bed), bee), bef), bfe) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bed, bee, bef), bed, bee, bef)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), ba), app(ty_[], cb))) → new_ltEs3(vyw4312, vyw4512, cb)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, app(app(ty_Either, ea), eb)), ba), cf)) → new_lt0(vyw4310, vyw4510, ea, eb)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, app(ty_Maybe, bce)), bcb)) → new_lt1(vyw4310, vyw4510, bce)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, bae), app(app(ty_@2, bbd), bbe))) → new_ltEs2(vyw4311, vyw4511, bbd, bbe)
new_compare23(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(ty_Either, beg), beh), bfe) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beg, beh), beg, beh)
new_ltEs1(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, hd), he), hf)) → new_ltEs(vyw4310, vyw4510, hd, he, hf)
new_primCompAux(vyw4300, vyw4500, vyw106, app(ty_[], bec)) → new_compare(vyw4300, vyw4500, bec)
new_ltEs1(Just(vyw4310), Just(vyw4510), app(app(ty_Either, hg), hh)) → new_ltEs0(vyw4310, vyw4510, hg, hh)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, app(ty_Maybe, ec)), ba), cf)) → new_lt1(vyw4310, vyw4510, ec)
new_compare23(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bfd, app(app(ty_Either, gb), app(app(ty_@2, ha), hb))) → new_ltEs2(vyw4310, vyw4510, ha, hb)
new_compare23(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bfd, app(ty_Maybe, app(ty_Maybe, baa))) → new_ltEs1(vyw4310, vyw4510, baa)
new_ltEs0(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, eg), eh), fa), fb) → new_ltEs(vyw4310, vyw4510, eg, eh, fa)
new_compare23(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bfd, app(app(ty_Either, app(ty_Maybe, ff)), fb)) → new_ltEs1(vyw4310, vyw4510, ff)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, app(app(app(ty_@3, bbg), bbh), bca)), bcb)) → new_lt(vyw4310, vyw4510, bbg, bbh, bca)
new_compare1(vyw430, vyw450, bed, bee, bef) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bed, bee, bef), bed, bee, bef)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(ty_@2, ed), ee), ba, cf) → new_lt2(vyw4310, vyw4510, ed, ee)
new_compare23(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bfd, app(app(ty_Either, app(app(app(ty_@3, eg), eh), fa)), fb)) → new_ltEs(vyw4310, vyw4510, eg, eh, fa)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), app(app(ty_@2, dc), dd)), cf)) → new_lt2(vyw4311, vyw4511, dc, dd)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(ty_Maybe, bce), bcb) → new_lt1(vyw4310, vyw4510, bce)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), ba), app(ty_Maybe, bg))) → new_ltEs1(vyw4312, vyw4512, bg)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, app(ty_[], ef)), ba), cf)) → new_lt3(vyw4310, vyw4510, ef)
new_ltEs0(Right(vyw4310), Right(vyw4510), gb, app(app(ty_Either, gf), gg)) → new_ltEs0(vyw4310, vyw4510, gf, gg)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, app(ty_Maybe, bbc)) → new_ltEs1(vyw4311, vyw4511, bbc)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(app(ty_@3, bbg), bbh), bca), bcb) → new_lt(vyw4310, vyw4510, bbg, bbh, bca)
new_ltEs0(Right(vyw4310), Right(vyw4510), gb, app(ty_[], hc)) → new_ltEs3(vyw4310, vyw4510, hc)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, app(app(app(ty_@3, cc), cd), ce), cf) → new_lt(vyw4311, vyw4511, cc, cd, ce)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, bae), app(app(ty_Either, bba), bbb))) → new_ltEs0(vyw4311, vyw4511, bba, bbb)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), app(app(app(ty_@3, cc), cd), ce)), cf)) → new_lt(vyw4311, vyw4511, cc, cd, ce)
new_ltEs0(Left(vyw4310), Left(vyw4510), app(app(ty_@2, fg), fh), fb) → new_ltEs2(vyw4310, vyw4510, fg, fh)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, app(ty_[], cb)) → new_ltEs3(vyw4312, vyw4512, cb)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, app(ty_[], bch)), bcb)) → new_lt3(vyw4310, vyw4510, bch)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, app(ty_[], de), cf) → new_lt3(vyw4311, vyw4511, de)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), ba), app(app(ty_@2, bh), ca))) → new_ltEs2(vyw4312, vyw4512, bh, ca)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), ba), app(app(app(ty_@3, bb), bc), bd))) → new_ltEs(vyw4312, vyw4512, bb, bc, bd)
new_compare23(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bfd, app(ty_Maybe, app(app(ty_Either, hg), hh))) → new_ltEs0(vyw4310, vyw4510, hg, hh)
new_ltEs0(Right(vyw4310), Right(vyw4510), gb, app(app(ty_@2, ha), hb)) → new_ltEs2(vyw4310, vyw4510, ha, hb)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, app(app(ty_Either, bba), bbb)) → new_ltEs0(vyw4311, vyw4511, bba, bbb)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(ty_[], ef), ba, cf) → new_lt3(vyw4310, vyw4510, ef)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, app(app(app(ty_@3, bb), bc), bd)) → new_ltEs(vyw4312, vyw4512, bb, bc, bd)
new_lt0(vyw430, vyw450, beg, beh) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beg, beh), beg, beh)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, app(ty_Maybe, db), cf) → new_lt1(vyw4311, vyw4511, db)
new_compare23(@2(vyw430, Left(vyw4310)), @2(vyw450, Left(vyw4510)), False, bfd, app(app(ty_Either, app(ty_[], ga)), fb)) → new_ltEs3(vyw4310, vyw4510, ga)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, app(app(ty_Either, cg), da), cf) → new_lt0(vyw4311, vyw4511, cg, da)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, bae), app(app(app(ty_@3, baf), bag), bah))) → new_ltEs(vyw4311, vyw4511, baf, bag, bah)
new_ltEs0(Left(vyw4310), Left(vyw4510), app(ty_[], ga), fb) → new_ltEs3(vyw4310, vyw4510, ga)
new_ltEs3(vyw431, vyw451, bda) → new_compare(vyw431, vyw451, bda)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, app(app(app(ty_@3, df), dg), dh)), ba), cf)) → new_lt(vyw4310, vyw4510, df, dg, dh)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), app(ty_Maybe, db)), cf)) → new_lt1(vyw4311, vyw4511, db)
new_primCompAux(vyw4300, vyw4500, vyw106, app(app(app(ty_@3, bdc), bdd), bde)) → new_compare1(vyw4300, vyw4500, bdc, bdd, bde)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, app(app(ty_@2, bh), ca)) → new_ltEs2(vyw4312, vyw4512, bh, ca)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, app(app(app(ty_@3, baf), bag), bah)) → new_ltEs(vyw4311, vyw4511, baf, bag, bah)
new_ltEs0(Right(vyw4310), Right(vyw4510), gb, app(app(app(ty_@3, gc), gd), ge)) → new_ltEs(vyw4310, vyw4510, gc, gd, ge)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(ty_Maybe, ec), ba, cf) → new_lt1(vyw4310, vyw4510, ec)
new_compare2(vyw430, vyw450, beg, beh) → new_compare21(vyw430, vyw450, new_esEs5(vyw430, vyw450, beg, beh), beg, beh)
new_compare23(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bfd, app(app(ty_Either, gb), app(app(app(ty_@3, gc), gd), ge))) → new_ltEs(vyw4310, vyw4510, gc, gd, ge)
new_ltEs1(Just(vyw4310), Just(vyw4510), app(ty_Maybe, baa)) → new_ltEs1(vyw4310, vyw4510, baa)
new_compare23(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bfd, app(app(ty_Either, gb), app(ty_Maybe, gh))) → new_ltEs1(vyw4310, vyw4510, gh)
new_compare23(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bfd, app(ty_Maybe, app(ty_[], bad))) → new_ltEs3(vyw4310, vyw4510, bad)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), app(app(ty_Either, bcc), bcd), bcb) → new_lt0(vyw4310, vyw4510, bcc, bcd)
new_compare21(vyw430, vyw450, False, beg, beh) → new_ltEs0(vyw430, vyw450, beg, beh)
new_compare22(vyw430, vyw450, False, bfa) → new_ltEs1(vyw430, vyw450, bfa)
new_ltEs0(Left(vyw4310), Left(vyw4510), app(app(ty_Either, fc), fd), fb) → new_ltEs0(vyw4310, vyw4510, fc, fd)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, bae), app(ty_[], bbf))) → new_ltEs3(vyw4311, vyw4511, bbf)
new_compare23(@2(:(vyw4300, vyw4301), vyw431), @2(:(vyw4500, vyw4501), vyw451), False, app(ty_[], bdb), bfe) → new_compare(vyw4301, vyw4501, bdb)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, app(ty_[], bbf)) → new_ltEs3(vyw4311, vyw4511, bbf)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, app(app(ty_Either, bcc), bcd)), bcb)) → new_lt0(vyw4310, vyw4510, bcc, bcd)
new_compare23(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(ty_Maybe, bfa), bfe) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfa), bfa)
new_lt2(vyw430, vyw450, bfb, bfc) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfb, bfc), bfb, bfc)
new_primCompAux(vyw4300, vyw4500, vyw106, app(app(ty_Either, bdf), bdg)) → new_compare2(vyw4300, vyw4500, bdf, bdg)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, app(app(ty_@2, dc), dd), cf) → new_lt2(vyw4311, vyw4511, dc, dd)
new_ltEs1(Just(vyw4310), Just(vyw4510), app(app(ty_@2, bab), bac)) → new_ltEs2(vyw4310, vyw4510, bab, bac)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(app(ty_@3, df), dg), dh), ba, cf) → new_lt(vyw4310, vyw4510, df, dg, dh)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, app(app(ty_@2, ed), ee)), ba), cf)) → new_lt2(vyw4310, vyw4510, ed, ee)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, app(ty_Maybe, bg)) → new_ltEs1(vyw4312, vyw4512, bg)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, app(app(ty_Either, be), bf)) → new_ltEs0(vyw4312, vyw4512, be, bf)
new_ltEs2(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, app(app(ty_@2, bbd), bbe)) → new_ltEs2(vyw4311, vyw4511, bbd, bbe)
new_compare(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bdb) → new_compare(vyw4301, vyw4501, bdb)
new_compare23(@2(vyw430, vyw431), @2(vyw450, vyw451), False, bfd, app(ty_[], bda)) → new_compare(vyw431, vyw451, bda)
new_compare23(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bfd, app(app(ty_Either, gb), app(app(ty_Either, gf), gg))) → new_ltEs0(vyw4310, vyw4510, gf, gg)
new_compare23(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bfd, app(ty_Maybe, app(app(app(ty_@3, hd), he), hf))) → new_ltEs(vyw4310, vyw4510, hd, he, hf)
new_compare(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bdb) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, bdb), bdb)
new_ltEs1(Just(vyw4310), Just(vyw4510), app(ty_[], bad)) → new_ltEs3(vyw4310, vyw4510, bad)
new_primCompAux(vyw4300, vyw4500, vyw106, app(app(ty_@2, bea), beb)) → new_compare4(vyw4300, vyw4500, bea, beb)
new_ltEs(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), app(app(ty_Either, ea), eb), ba, cf) → new_lt0(vyw4310, vyw4510, ea, eb)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), ba), app(app(ty_Either, be), bf))) → new_ltEs0(vyw4312, vyw4512, be, bf)
new_compare23(@2(vyw430, Just(vyw4310)), @2(vyw450, Just(vyw4510)), False, bfd, app(ty_Maybe, app(app(ty_@2, bab), bac))) → new_ltEs2(vyw4310, vyw4510, bab, bac)
new_compare23(@2(vyw430, @3(vyw4310, vyw4311, vyw4312)), @2(vyw450, @3(vyw4510, vyw4511, vyw4512)), False, bfd, app(app(app(ty_@3, h), app(ty_[], de)), cf)) → new_lt3(vyw4311, vyw4511, de)
new_lt3(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bdb) → new_compare(vyw4301, vyw4501, bdb)
new_compare23(@2(:(vyw4300, vyw4301), vyw431), @2(:(vyw4500, vyw4501), vyw451), False, app(ty_[], bdb), bfe) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, bdb), bdb)
new_compare23(@2(vyw430, Right(vyw4310)), @2(vyw450, Right(vyw4510)), False, bfd, app(app(ty_Either, gb), app(ty_[], hc))) → new_ltEs3(vyw4310, vyw4510, hc)
new_compare4(vyw430, vyw450, bfb, bfc) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfb, bfc), bfb, bfc)
new_ltEs0(Right(vyw4310), Right(vyw4510), gb, app(ty_Maybe, gh)) → new_ltEs1(vyw4310, vyw4510, gh)
new_lt(vyw430, vyw450, bed, bee, bef) → new_compare20(vyw430, vyw450, new_esEs4(vyw430, vyw450, bed, bee, bef), bed, bee, bef)
new_compare3(vyw430, vyw450, bfa) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfa), bfa)
new_compare23(@2(vyw430, vyw431), @2(vyw450, vyw451), False, app(app(ty_@2, bfb), bfc), bfe) → new_compare23(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfb, bfc), bfb, bfc)
new_primCompAux(vyw4300, vyw4500, vyw106, app(ty_Maybe, bdh)) → new_compare3(vyw4300, vyw4500, bdh)
new_lt3(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bdb) → new_primCompAux(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, bdb), bdb)
new_compare23(@2(vyw430, @2(vyw4310, vyw4311)), @2(vyw450, @2(vyw4510, vyw4511)), False, bfd, app(app(ty_@2, bae), app(ty_Maybe, bbc))) → new_ltEs1(vyw4311, vyw4511, bbc)
new_ltEs0(Left(vyw4310), Left(vyw4510), app(ty_Maybe, ff), fb) → new_ltEs1(vyw4310, vyw4510, ff)
new_lt1(vyw430, vyw450, bfa) → new_compare22(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfa), bfa)

The TRS R consists of the following rules:

new_esEs25(vyw430, vyw450, app(ty_[], bdb)) → new_esEs14(vyw430, vyw450, bdb)
new_esEs19(:%(vyw300, vyw301), :%(vyw4000, vyw4001), ceg) → new_asAs(new_esEs23(vyw300, vyw4000, ceg), new_esEs24(vyw301, vyw4001, ceg))
new_lt4(vyw430, vyw450) → new_esEs8(new_compare5(vyw430, vyw450), LT)
new_compare31(vyw4300, vyw4500, ty_Double) → new_compare15(vyw4300, vyw4500)
new_lt16(vyw430, vyw450, ty_Int) → new_lt5(vyw430, vyw450)
new_esEs18(Char(vyw300), Char(vyw4000)) → new_primEqNat0(vyw300, vyw4000)
new_lt19(vyw4310, vyw4510, app(app(ty_Either, bcc), bcd)) → new_lt10(vyw4310, vyw4510, bcc, bcd)
new_esEs10(vyw301, vyw4001, app(app(app(ty_@3, bhe), bhf), bhg)) → new_esEs4(vyw301, vyw4001, bhe, bhf, bhg)
new_ltEs4(EQ, GT) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(ty_Maybe, gh)) → new_ltEs6(vyw4310, vyw4510, gh)
new_esEs20(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_compare10(vyw430, vyw450, True, beg, beh) → LT
new_ltEs13(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), bae, bcb) → new_pePe(new_lt19(vyw4310, vyw4510, bae), new_asAs(new_esEs27(vyw4310, vyw4510, bae), new_ltEs19(vyw4311, vyw4511, bcb)))
new_esEs20(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_lt21(vyw4310, vyw4510, app(ty_Maybe, ec)) → new_lt7(vyw4310, vyw4510, ec)
new_ltEs19(vyw4311, vyw4511, ty_Float) → new_ltEs11(vyw4311, vyw4511)
new_ltEs6(Nothing, Just(vyw4510), cgd) → True
new_ltEs20(vyw4312, vyw4512, app(ty_[], cb)) → new_ltEs7(vyw4312, vyw4512, cb)
new_compare14(vyw430, vyw450, True, bed, bee, bef) → LT
new_compare31(vyw4300, vyw4500, ty_Int) → new_compare8(vyw4300, vyw4500)
new_lt20(vyw4311, vyw4511, ty_@0) → new_lt6(vyw4311, vyw4511)
new_esEs26(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_ltEs9(vyw431, vyw451) → new_not(new_esEs8(new_compare13(vyw431, vyw451), GT))
new_esEs21(vyw301, vyw4001, ty_@0) → new_esEs17(vyw301, vyw4001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(vyw4310, vyw4510, app(ty_Ratio, dac)) → new_esEs19(vyw4310, vyw4510, dac)
new_ltEs20(vyw4312, vyw4512, ty_@0) → new_ltEs15(vyw4312, vyw4512)
new_esEs27(vyw4310, vyw4510, app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs4(vyw4310, vyw4510, bbg, bbh, bca)
new_sr(Integer(vyw43000), Integer(vyw45010)) → Integer(new_primMulInt(vyw43000, vyw45010))
new_esEs12(True, True) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_@0, fb) → new_ltEs15(vyw4310, vyw4510)
new_compare25(vyw430, vyw450, True, bfa) → EQ
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Ordering, fb) → new_ltEs4(vyw4310, vyw4510)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_@0) → new_esEs17(vyw302, vyw4002)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_Ratio, dbf), dae) → new_esEs19(vyw300, vyw4000, dbf)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Bool, dae) → new_esEs12(vyw300, vyw4000)
new_ltEs8(vyw431, vyw451) → new_not(new_esEs8(new_compare7(vyw431, vyw451), GT))
new_esEs22(vyw302, vyw4002, app(ty_Ratio, cec)) → new_esEs19(vyw302, vyw4002, cec)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(ty_@2, fg), fh), fb) → new_ltEs13(vyw4310, vyw4510, fg, fh)
new_esEs4(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), cad, cae, caf) → new_asAs(new_esEs20(vyw300, vyw4000, cad), new_asAs(new_esEs21(vyw301, vyw4001, cae), new_esEs22(vyw302, vyw4002, caf)))
new_compare5(vyw430, vyw450) → new_compare26(vyw430, vyw450, new_esEs8(vyw430, vyw450))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Float) → new_ltEs11(vyw4310, vyw4510)
new_ltEs5(Left(vyw4310), Right(vyw4510), gb, fb) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(ty_Ratio, cef)) → new_ltEs17(vyw4310, vyw4510, cef)
new_lt17(vyw430, vyw450) → new_esEs8(new_compare13(vyw430, vyw450), LT)
new_esEs22(vyw302, vyw4002, app(ty_Maybe, ced)) → new_esEs6(vyw302, vyw4002, ced)
new_lt9(vyw430, vyw450, bdb) → new_esEs8(new_compare0(vyw430, vyw450, bdb), LT)
new_esEs27(vyw4310, vyw4510, app(ty_Maybe, bce)) → new_esEs6(vyw4310, vyw4510, bce)
new_lt16(vyw430, vyw450, ty_Char) → new_lt17(vyw430, vyw450)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(ty_@2, cfb), cfc)) → new_esEs7(vyw300, vyw4000, cfb, cfc)
new_esEs29(vyw4311, vyw4511, app(ty_Ratio, ddf)) → new_esEs19(vyw4311, vyw4511, ddf)
new_esEs25(vyw430, vyw450, ty_Double) → new_esEs15(vyw430, vyw450)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(app(ty_@3, dba), dbb), dbc), dae) → new_esEs4(vyw300, vyw4000, dba, dbb, dbc)
new_compare31(vyw4300, vyw4500, app(app(app(ty_@3, bdc), bdd), bde)) → new_compare30(vyw4300, vyw4500, bdc, bdd, bde)
new_compare110(vyw86, vyw87, vyw88, vyw89, True, vyw91, ddc, ddd) → new_compare111(vyw86, vyw87, vyw88, vyw89, True, ddc, ddd)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(app(ty_Either, gf), gg)) → new_ltEs5(vyw4310, vyw4510, gf, gg)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, app(ty_[], cdc)) → new_esEs14(vyw302, vyw4002, cdc)
new_ltEs18(vyw431, vyw451, app(ty_[], bda)) → new_ltEs7(vyw431, vyw451, bda)
new_compare29(vyw430, vyw450) → new_compare210(vyw430, vyw450, new_esEs12(vyw430, vyw450))
new_ltEs5(Right(vyw4310), Left(vyw4510), gb, fb) → False
new_lt20(vyw4311, vyw4511, ty_Bool) → new_lt14(vyw4311, vyw4511)
new_esEs17(@0, @0) → True
new_lt21(vyw4310, vyw4510, app(app(ty_@2, ed), ee)) → new_lt12(vyw4310, vyw4510, ed, ee)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_@2, bab), bac)) → new_ltEs13(vyw4310, vyw4510, bab, bac)
new_esEs25(vyw430, vyw450, ty_Float) → new_esEs13(vyw430, vyw450)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_Ratio, cee), fb) → new_ltEs17(vyw4310, vyw4510, cee)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_Maybe, dbg), dae) → new_esEs6(vyw300, vyw4000, dbg)
new_pePe(False, vyw105) → vyw105
new_esEs14([], [], cgh) → True
new_esEs25(vyw430, vyw450, app(app(ty_@2, bfb), bfc)) → new_esEs7(vyw430, vyw450, bfb, bfc)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Integer, fb) → new_ltEs8(vyw4310, vyw4510)
new_lt7(vyw430, vyw450, bfa) → new_esEs8(new_compare16(vyw430, vyw450, bfa), LT)
new_ltEs12(True, False) → False
new_esEs10(vyw301, vyw4001, ty_Bool) → new_esEs12(vyw301, vyw4001)
new_esEs29(vyw4311, vyw4511, ty_Char) → new_esEs18(vyw4311, vyw4511)
new_esEs29(vyw4311, vyw4511, app(ty_[], de)) → new_esEs14(vyw4311, vyw4511, de)
new_lt19(vyw4310, vyw4510, app(ty_Maybe, bce)) → new_lt7(vyw4310, vyw4510, bce)
new_lt6(vyw430, vyw450) → new_esEs8(new_compare9(vyw430, vyw450), LT)
new_lt18(vyw430, vyw450, cgf) → new_esEs8(new_compare6(vyw430, vyw450, cgf), LT)
new_esEs29(vyw4311, vyw4511, ty_@0) → new_esEs17(vyw4311, vyw4511)
new_lt19(vyw4310, vyw4510, app(ty_[], bch)) → new_lt9(vyw4310, vyw4510, bch)
new_compare31(vyw4300, vyw4500, ty_Bool) → new_compare29(vyw4300, vyw4500)
new_lt21(vyw4310, vyw4510, app(ty_Ratio, dde)) → new_lt18(vyw4310, vyw4510, dde)
new_compare27(vyw430, vyw450, False, bed, bee, bef) → new_compare14(vyw430, vyw450, new_ltEs10(vyw430, vyw450, bed, bee, bef), bed, bee, bef)
new_esEs26(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Double) → new_esEs15(vyw302, vyw4002)
new_esEs26(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Int) → new_esEs11(vyw302, vyw4002)
new_esEs21(vyw301, vyw4001, app(ty_Ratio, cda)) → new_esEs19(vyw301, vyw4001, cda)
new_esEs28(vyw4310, vyw4510, app(app(app(ty_@3, df), dg), dh)) → new_esEs4(vyw4310, vyw4510, df, dg, dh)
new_lt16(vyw430, vyw450, ty_Bool) → new_lt14(vyw430, vyw450)
new_esEs21(vyw301, vyw4001, ty_Double) → new_esEs15(vyw301, vyw4001)
new_ltEs18(vyw431, vyw451, ty_Int) → new_ltEs16(vyw431, vyw451)
new_esEs22(vyw302, vyw4002, ty_Ordering) → new_esEs8(vyw302, vyw4002)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Int, dae) → new_esEs11(vyw300, vyw4000)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Ordering, dae) → new_esEs8(vyw300, vyw4000)
new_ltEs10(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), h, ba, cf) → new_pePe(new_lt21(vyw4310, vyw4510, h), new_asAs(new_esEs28(vyw4310, vyw4510, h), new_pePe(new_lt20(vyw4311, vyw4511, ba), new_asAs(new_esEs29(vyw4311, vyw4511, ba), new_ltEs20(vyw4312, vyw4512, cf)))))
new_lt19(vyw4310, vyw4510, ty_Int) → new_lt5(vyw4310, vyw4510)
new_primCmpNat0(Zero, Succ(vyw45000)) → LT
new_ltEs20(vyw4312, vyw4512, ty_Double) → new_ltEs14(vyw4312, vyw4512)
new_esEs9(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs25(vyw430, vyw450, app(app(ty_Either, beg), beh)) → new_esEs5(vyw430, vyw450, beg, beh)
new_esEs8(LT, LT) → True
new_lt16(vyw430, vyw450, ty_Ordering) → new_lt4(vyw430, vyw450)
new_lt20(vyw4311, vyw4511, ty_Int) → new_lt5(vyw4311, vyw4511)
new_esEs25(vyw430, vyw450, ty_Ordering) → new_esEs8(vyw430, vyw450)
new_esEs29(vyw4311, vyw4511, app(app(ty_@2, dc), dd)) → new_esEs7(vyw4311, vyw4511, dc, dd)
new_esEs28(vyw4310, vyw4510, ty_Double) → new_esEs15(vyw4310, vyw4510)
new_esEs28(vyw4310, vyw4510, ty_Integer) → new_esEs16(vyw4310, vyw4510)
new_lt11(vyw430, vyw450) → new_esEs8(new_compare19(vyw430, vyw450), LT)
new_esEs10(vyw301, vyw4001, app(ty_Ratio, cab)) → new_esEs19(vyw301, vyw4001, cab)
new_pePe(True, vyw105) → True
new_compare0([], [], bdb) → EQ
new_primEqNat0(Zero, Zero) → True
new_compare31(vyw4300, vyw4500, app(app(ty_Either, bdf), bdg)) → new_compare18(vyw4300, vyw4500, bdf, bdg)
new_esEs20(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_compare26(vyw430, vyw450, True) → EQ
new_compare31(vyw4300, vyw4500, app(ty_Ratio, cgc)) → new_compare6(vyw4300, vyw4500, cgc)
new_esEs29(vyw4311, vyw4511, app(ty_Maybe, db)) → new_esEs6(vyw4311, vyw4511, db)
new_ltEs12(False, False) → True
new_ltEs20(vyw4312, vyw4512, ty_Ordering) → new_ltEs4(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, ty_Bool) → new_lt14(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, app(ty_Maybe, dab)) → new_esEs6(vyw300, vyw4000, dab)
new_compare11(vyw430, vyw450, True, bfa) → LT
new_primMulNat0(Succ(vyw30000), Succ(vyw400000)) → new_primPlusNat1(new_primMulNat0(vyw30000, Succ(vyw400000)), vyw400000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Char) → new_ltEs9(vyw4310, vyw4510)
new_ltEs18(vyw431, vyw451, ty_Char) → new_ltEs9(vyw431, vyw451)
new_lt20(vyw4311, vyw4511, app(ty_[], de)) → new_lt9(vyw4311, vyw4511, de)
new_esEs9(vyw300, vyw4000, app(app(app(ty_@3, bgc), bgd), bge)) → new_esEs4(vyw300, vyw4000, bgc, bgd, bge)
new_esEs22(vyw302, vyw4002, app(app(ty_@2, cdd), cde)) → new_esEs7(vyw302, vyw4002, cdd, cde)
new_esEs9(vyw300, vyw4000, app(ty_Maybe, bha)) → new_esEs6(vyw300, vyw4000, bha)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Float) → new_esEs13(vyw300, vyw4000)
new_lt19(vyw4310, vyw4510, ty_Double) → new_lt13(vyw4310, vyw4510)
new_ltEs18(vyw431, vyw451, app(app(app(ty_@3, h), ba), cf)) → new_ltEs10(vyw431, vyw451, h, ba, cf)
new_esEs6(Just(vyw300), Just(vyw4000), ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs26(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs8(GT, GT) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Bool, fb) → new_ltEs12(vyw4310, vyw4510)
new_esEs12(False, False) → True
new_ltEs19(vyw4311, vyw4511, ty_Bool) → new_ltEs12(vyw4311, vyw4511)
new_esEs26(vyw300, vyw4000, app(app(app(ty_@3, chd), che), chf)) → new_esEs4(vyw300, vyw4000, chd, che, chf)
new_ltEs18(vyw431, vyw451, app(app(ty_Either, gb), fb)) → new_ltEs5(vyw431, vyw451, gb, fb)
new_compare110(vyw86, vyw87, vyw88, vyw89, False, vyw91, ddc, ddd) → new_compare111(vyw86, vyw87, vyw88, vyw89, vyw91, ddc, ddd)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_lt20(vyw4311, vyw4511, ty_Char) → new_lt17(vyw4311, vyw4511)
new_lt19(vyw4310, vyw4510, app(app(app(ty_@3, bbg), bbh), bca)) → new_lt15(vyw4310, vyw4510, bbg, bbh, bca)
new_ltEs20(vyw4312, vyw4512, ty_Int) → new_ltEs16(vyw4312, vyw4512)
new_esEs13(Float(vyw300, vyw301), Float(vyw4000, vyw4001)) → new_esEs11(new_sr0(vyw300, vyw4000), new_sr0(vyw301, vyw4001))
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Char) → new_ltEs9(vyw4310, vyw4510)
new_primEqInt(Neg(Succ(vyw3000)), Neg(Succ(vyw40000))) → new_primEqNat0(vyw3000, vyw40000)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Integer, dae) → new_esEs16(vyw300, vyw4000)
new_ltEs19(vyw4311, vyw4511, ty_Integer) → new_ltEs8(vyw4311, vyw4511)
new_esEs20(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_ltEs20(vyw4312, vyw4512, ty_Char) → new_ltEs9(vyw4312, vyw4512)
new_esEs9(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Double) → new_ltEs14(vyw4310, vyw4510)
new_ltEs19(vyw4311, vyw4511, app(ty_Ratio, dad)) → new_ltEs17(vyw4311, vyw4511, dad)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_[], daf), dae) → new_esEs14(vyw300, vyw4000, daf)
new_esEs28(vyw4310, vyw4510, ty_@0) → new_esEs17(vyw4310, vyw4510)
new_ltEs20(vyw4312, vyw4512, ty_Bool) → new_ltEs12(vyw4312, vyw4512)
new_lt16(vyw430, vyw450, app(ty_Maybe, bfa)) → new_lt7(vyw430, vyw450, bfa)
new_esEs29(vyw4311, vyw4511, app(app(ty_Either, cg), da)) → new_esEs5(vyw4311, vyw4511, cg, da)
new_compare28(vyw430, vyw450, bfb, bfc) → new_compare211(vyw430, vyw450, new_esEs7(vyw430, vyw450, bfb, bfc), bfb, bfc)
new_esEs14([], :(vyw4000, vyw4001), cgh) → False
new_esEs14(:(vyw300, vyw301), [], cgh) → False
new_esEs9(vyw300, vyw4000, app(ty_[], bfh)) → new_esEs14(vyw300, vyw4000, bfh)
new_compare111(vyw86, vyw87, vyw88, vyw89, True, ddc, ddd) → LT
new_esEs25(vyw430, vyw450, ty_Char) → new_esEs18(vyw430, vyw450)
new_compare31(vyw4300, vyw4500, ty_Integer) → new_compare7(vyw4300, vyw4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs19(vyw4311, vyw4511, ty_Ordering) → new_ltEs4(vyw4311, vyw4511)
new_esEs21(vyw301, vyw4001, app(app(ty_@2, ccb), ccc)) → new_esEs7(vyw301, vyw4001, ccb, ccc)
new_lt15(vyw430, vyw450, bed, bee, bef) → new_esEs8(new_compare30(vyw430, vyw450, bed, bee, bef), LT)
new_esEs20(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs27(vyw4310, vyw4510, app(app(ty_Either, bcc), bcd)) → new_esEs5(vyw4310, vyw4510, bcc, bcd)
new_lt16(vyw430, vyw450, app(ty_Ratio, cgf)) → new_lt18(vyw430, vyw450, cgf)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(ty_Ratio, dda)) → new_esEs19(vyw300, vyw4000, dda)
new_ltEs20(vyw4312, vyw4512, app(ty_Ratio, ddg)) → new_ltEs17(vyw4312, vyw4512, ddg)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs26(vyw300, vyw4000, app(ty_[], cha)) → new_esEs14(vyw300, vyw4000, cha)
new_esEs9(vyw300, vyw4000, app(ty_Ratio, bgh)) → new_esEs19(vyw300, vyw4000, bgh)
new_compare8(vyw430, vyw450) → new_primCmpInt(vyw430, vyw450)
new_primEqInt(Neg(Succ(vyw3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vyw40000))) → False
new_primCompAux0(vyw114, GT) → GT
new_lt20(vyw4311, vyw4511, ty_Integer) → new_lt8(vyw4311, vyw4511)
new_esEs8(EQ, EQ) → True
new_primPlusNat1(Zero, vyw400000) → Succ(vyw400000)
new_esEs23(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Float) → new_esEs13(vyw302, vyw4002)
new_esEs20(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_compare24(vyw430, vyw450, True, beg, beh) → EQ
new_esEs25(vyw430, vyw450, app(ty_Ratio, cgf)) → new_esEs19(vyw430, vyw450, cgf)
new_esEs28(vyw4310, vyw4510, app(ty_[], ef)) → new_esEs14(vyw4310, vyw4510, ef)
new_esEs20(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_lt21(vyw4310, vyw4510, app(ty_[], ef)) → new_lt9(vyw4310, vyw4510, ef)
new_lt19(vyw4310, vyw4510, ty_Float) → new_lt11(vyw4310, vyw4510)
new_ltEs11(vyw431, vyw451) → new_not(new_esEs8(new_compare19(vyw431, vyw451), GT))
new_ltEs18(vyw431, vyw451, ty_Ordering) → new_ltEs4(vyw431, vyw451)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_ltEs4(EQ, LT) → False
new_lt16(vyw430, vyw450, ty_@0) → new_lt6(vyw430, vyw450)
new_esEs25(vyw430, vyw450, ty_@0) → new_esEs17(vyw430, vyw450)
new_esEs28(vyw4310, vyw4510, app(app(ty_@2, ed), ee)) → new_esEs7(vyw4310, vyw4510, ed, ee)
new_esEs29(vyw4311, vyw4511, ty_Float) → new_esEs13(vyw4311, vyw4511)
new_lt5(vyw430, vyw450) → new_esEs8(new_compare8(vyw430, vyw450), LT)
new_primCmpNat0(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat0(vyw43000, vyw45000)
new_ltEs17(vyw431, vyw451, cgg) → new_not(new_esEs8(new_compare6(vyw431, vyw451, cgg), GT))
new_lt19(vyw4310, vyw4510, ty_Integer) → new_lt8(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_compare11(vyw430, vyw450, False, bfa) → GT
new_esEs6(Nothing, Nothing, ceh) → True
new_primEqInt(Pos(Succ(vyw3000)), Pos(Succ(vyw40000))) → new_primEqNat0(vyw3000, vyw40000)
new_compare10(vyw430, vyw450, False, beg, beh) → GT
new_lt19(vyw4310, vyw4510, app(app(ty_@2, bcf), bcg)) → new_lt12(vyw4310, vyw4510, bcf, bcg)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(ty_Either, fc), fd), fb) → new_ltEs5(vyw4310, vyw4510, fc, fd)
new_esEs21(vyw301, vyw4001, app(ty_Maybe, cdb)) → new_esEs6(vyw301, vyw4001, cdb)
new_esEs9(vyw300, vyw4000, app(app(ty_@2, bga), bgb)) → new_esEs7(vyw300, vyw4000, bga, bgb)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(app(ty_Either, dcg), dch)) → new_esEs5(vyw300, vyw4000, dcg, dch)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Int) → new_esEs11(vyw300, vyw4000)
new_esEs6(Just(vyw300), Nothing, ceh) → False
new_esEs6(Nothing, Just(vyw4000), ceh) → False
new_primEqNat0(Succ(vyw3000), Succ(vyw40000)) → new_primEqNat0(vyw3000, vyw40000)
new_esEs27(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Integer) → new_ltEs8(vyw4310, vyw4510)
new_esEs21(vyw301, vyw4001, app(ty_[], cca)) → new_esEs14(vyw301, vyw4001, cca)
new_compare31(vyw4300, vyw4500, app(app(ty_@2, bea), beb)) → new_compare28(vyw4300, vyw4500, bea, beb)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Bool) → new_ltEs12(vyw4310, vyw4510)
new_ltEs14(vyw431, vyw451) → new_not(new_esEs8(new_compare15(vyw431, vyw451), GT))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Int) → new_ltEs16(vyw4310, vyw4510)
new_esEs10(vyw301, vyw4001, ty_Double) → new_esEs15(vyw301, vyw4001)
new_ltEs19(vyw4311, vyw4511, ty_Double) → new_ltEs14(vyw4311, vyw4511)
new_esEs22(vyw302, vyw4002, ty_Bool) → new_esEs12(vyw302, vyw4002)
new_ltEs4(GT, EQ) → False
new_esEs28(vyw4310, vyw4510, ty_Int) → new_esEs11(vyw4310, vyw4510)
new_primCmpInt(Neg(Succ(vyw43000)), Neg(vyw4500)) → new_primCmpNat0(vyw4500, Succ(vyw43000))
new_esEs10(vyw301, vyw4001, app(app(ty_@2, bhc), bhd)) → new_esEs7(vyw301, vyw4001, bhc, bhd)
new_esEs21(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_esEs28(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, ty_Double) → new_lt13(vyw4310, vyw4510)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(vyw3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vyw40000))) → False
new_ltEs16(vyw431, vyw451) → new_not(new_esEs8(new_compare8(vyw431, vyw451), GT))
new_ltEs19(vyw4311, vyw4511, app(ty_Maybe, bbc)) → new_ltEs6(vyw4311, vyw4511, bbc)
new_ltEs4(EQ, EQ) → True
new_primPlusNat0(Succ(vyw7700), Zero) → Succ(vyw7700)
new_primPlusNat0(Zero, Succ(vyw4000000)) → Succ(vyw4000000)
new_ltEs18(vyw431, vyw451, ty_Float) → new_ltEs11(vyw431, vyw451)
new_ltEs6(Just(vyw4310), Nothing, cgd) → False
new_primCmpNat0(Zero, Zero) → EQ
new_primCmpNat0(Succ(vyw43000), Zero) → GT
new_esEs5(Left(vyw300), Left(vyw4000), ty_Char, dae) → new_esEs18(vyw300, vyw4000)
new_compare16(vyw430, vyw450, bfa) → new_compare25(vyw430, vyw450, new_esEs6(vyw430, vyw450, bfa), bfa)
new_esEs20(vyw300, vyw4000, app(app(app(ty_@3, cbb), cbc), cbd)) → new_esEs4(vyw300, vyw4000, cbb, cbc, cbd)
new_primCmpInt(Neg(Zero), Pos(Succ(vyw45000))) → LT
new_esEs29(vyw4311, vyw4511, app(app(app(ty_@3, cc), cd), ce)) → new_esEs4(vyw4311, vyw4511, cc, cd, ce)
new_compare9(@0, @0) → EQ
new_esEs20(vyw300, vyw4000, app(app(ty_Either, cbe), cbf)) → new_esEs5(vyw300, vyw4000, cbe, cbf)
new_ltEs4(GT, LT) → False
new_esEs28(vyw4310, vyw4510, app(ty_Ratio, dde)) → new_esEs19(vyw4310, vyw4510, dde)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Float, dae) → new_esEs13(vyw300, vyw4000)
new_compare14(vyw430, vyw450, False, bed, bee, bef) → GT
new_lt21(vyw4310, vyw4510, ty_Integer) → new_lt8(vyw4310, vyw4510)
new_esEs10(vyw301, vyw4001, ty_Char) → new_esEs18(vyw301, vyw4001)
new_primEqInt(Pos(Succ(vyw3000)), Neg(vyw4000)) → False
new_primEqInt(Neg(Succ(vyw3000)), Pos(vyw4000)) → False
new_esEs28(vyw4310, vyw4510, app(app(ty_Either, ea), eb)) → new_esEs5(vyw4310, vyw4510, ea, eb)
new_esEs10(vyw301, vyw4001, app(ty_[], bhb)) → new_esEs14(vyw301, vyw4001, bhb)
new_ltEs19(vyw4311, vyw4511, ty_@0) → new_ltEs15(vyw4311, vyw4511)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Integer) → new_esEs16(vyw300, vyw4000)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Double, fb) → new_ltEs14(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Maybe, baa)) → new_ltEs6(vyw4310, vyw4510, baa)
new_esEs9(vyw300, vyw4000, app(app(ty_Either, bgf), bgg)) → new_esEs5(vyw300, vyw4000, bgf, bgg)
new_esEs28(vyw4310, vyw4510, app(ty_Maybe, ec)) → new_esEs6(vyw4310, vyw4510, ec)
new_primEqInt(Pos(Zero), Neg(Succ(vyw40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vyw40000))) → False
new_primCmpInt(Pos(Zero), Pos(Succ(vyw45000))) → new_primCmpNat0(Zero, Succ(vyw45000))
new_esEs27(vyw4310, vyw4510, app(app(ty_@2, bcf), bcg)) → new_esEs7(vyw4310, vyw4510, bcf, bcg)
new_lt21(vyw4310, vyw4510, ty_Char) → new_lt17(vyw4310, vyw4510)
new_compare12(vyw430, vyw450, False) → GT
new_lt20(vyw4311, vyw4511, ty_Ordering) → new_lt4(vyw4311, vyw4511)
new_compare31(vyw4300, vyw4500, ty_Ordering) → new_compare5(vyw4300, vyw4500)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_ltEs18(vyw431, vyw451, ty_@0) → new_ltEs15(vyw431, vyw451)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs21(vyw301, vyw4001, ty_Char) → new_esEs18(vyw301, vyw4001)
new_lt16(vyw430, vyw450, app(app(app(ty_@3, bed), bee), bef)) → new_lt15(vyw430, vyw450, bed, bee, bef)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(app(app(ty_@3, gc), gd), ge)) → new_ltEs10(vyw4310, vyw4510, gc, gd, ge)
new_primCompAux0(vyw114, LT) → LT
new_esEs9(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_lt8(vyw430, vyw450) → new_esEs8(new_compare7(vyw430, vyw450), LT)
new_ltEs19(vyw4311, vyw4511, app(app(ty_@2, bbd), bbe)) → new_ltEs13(vyw4311, vyw4511, bbd, bbe)
new_esEs11(vyw30, vyw400) → new_primEqInt(vyw30, vyw400)
new_not(False) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Int) → new_ltEs16(vyw4310, vyw4510)
new_lt16(vyw430, vyw450, app(app(ty_@2, bfb), bfc)) → new_lt12(vyw430, vyw450, bfb, bfc)
new_primCmpInt(Pos(Succ(vyw43000)), Pos(vyw4500)) → new_primCmpNat0(Succ(vyw43000), vyw4500)
new_lt16(vyw430, vyw450, ty_Float) → new_lt11(vyw430, vyw450)
new_ltEs15(vyw431, vyw451) → new_not(new_esEs8(new_compare9(vyw431, vyw451), GT))
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_Either, hg), hh)) → new_ltEs5(vyw4310, vyw4510, hg, hh)
new_lt20(vyw4311, vyw4511, app(app(app(ty_@3, cc), cd), ce)) → new_lt15(vyw4311, vyw4511, cc, cd, ce)
new_lt14(vyw430, vyw450) → new_esEs8(new_compare29(vyw430, vyw450), LT)
new_compare17(vyw430, vyw450, True) → LT
new_esEs25(vyw430, vyw450, app(app(app(ty_@3, bed), bee), bef)) → new_esEs4(vyw430, vyw450, bed, bee, bef)
new_esEs9(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_lt20(vyw4311, vyw4511, ty_Double) → new_lt13(vyw4311, vyw4511)
new_compare0(:(vyw4300, vyw4301), [], bdb) → GT
new_compare31(vyw4300, vyw4500, ty_@0) → new_compare9(vyw4300, vyw4500)
new_lt21(vyw4310, vyw4510, ty_Int) → new_lt5(vyw4310, vyw4510)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(ty_[], hc)) → new_ltEs7(vyw4310, vyw4510, hc)
new_esEs22(vyw302, vyw4002, app(app(app(ty_@3, cdf), cdg), cdh)) → new_esEs4(vyw302, vyw4002, cdf, cdg, cdh)
new_esEs26(vyw300, vyw4000, app(app(ty_Either, chg), chh)) → new_esEs5(vyw300, vyw4000, chg, chh)
new_lt19(vyw4310, vyw4510, app(ty_Ratio, dac)) → new_lt18(vyw4310, vyw4510, dac)
new_ltEs18(vyw431, vyw451, ty_Bool) → new_ltEs12(vyw431, vyw451)
new_esEs27(vyw4310, vyw4510, ty_Int) → new_esEs11(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Bool) → new_ltEs12(vyw4310, vyw4510)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Double, dae) → new_esEs15(vyw300, vyw4000)
new_primCmpInt(Pos(Succ(vyw43000)), Neg(vyw4500)) → GT
new_esEs22(vyw302, vyw4002, ty_Char) → new_esEs18(vyw302, vyw4002)
new_esEs21(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_lt19(vyw4310, vyw4510, ty_Char) → new_lt17(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_primMulInt(Pos(vyw3000), Pos(vyw40000)) → Pos(new_primMulNat0(vyw3000, vyw40000))
new_esEs24(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_esEs10(vyw301, vyw4001, ty_@0) → new_esEs17(vyw301, vyw4001)
new_compare24(vyw430, vyw450, False, beg, beh) → new_compare10(vyw430, vyw450, new_ltEs5(vyw430, vyw450, beg, beh), beg, beh)
new_esEs5(Left(vyw300), Left(vyw4000), ty_@0, dae) → new_esEs17(vyw300, vyw4000)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(app(app(ty_@3, dcd), dce), dcf)) → new_esEs4(vyw300, vyw4000, dcd, dce, dcf)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_[], cfa)) → new_esEs14(vyw300, vyw4000, cfa)
new_lt20(vyw4311, vyw4511, app(app(ty_Either, cg), da)) → new_lt10(vyw4311, vyw4511, cg, da)
new_esEs27(vyw4310, vyw4510, ty_Double) → new_esEs15(vyw4310, vyw4510)
new_esEs15(Double(vyw300, vyw301), Double(vyw4000, vyw4001)) → new_esEs11(new_sr0(vyw300, vyw4000), new_sr0(vyw301, vyw4001))
new_esEs5(Left(vyw300), Right(vyw4000), dbh, dae) → False
new_esEs5(Right(vyw300), Left(vyw4000), dbh, dae) → False
new_primMulInt(Neg(vyw3000), Neg(vyw40000)) → Pos(new_primMulNat0(vyw3000, vyw40000))
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs10(vyw301, vyw4001, ty_Float) → new_esEs13(vyw301, vyw4001)
new_ltEs19(vyw4311, vyw4511, app(app(ty_Either, bba), bbb)) → new_ltEs5(vyw4311, vyw4511, bba, bbb)
new_primEqNat0(Succ(vyw3000), Zero) → False
new_primEqNat0(Zero, Succ(vyw40000)) → False
new_primPlusNat0(Zero, Zero) → Zero
new_lt20(vyw4311, vyw4511, app(app(ty_@2, dc), dd)) → new_lt12(vyw4311, vyw4511, dc, dd)
new_esEs26(vyw300, vyw4000, app(app(ty_@2, chb), chc)) → new_esEs7(vyw300, vyw4000, chb, chc)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_Ratio, cga)) → new_esEs19(vyw300, vyw4000, cga)
new_esEs25(vyw430, vyw450, app(ty_Maybe, bfa)) → new_esEs6(vyw430, vyw450, bfa)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Double) → new_ltEs14(vyw4310, vyw4510)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Float, fb) → new_ltEs11(vyw4310, vyw4510)
new_esEs20(vyw300, vyw4000, app(ty_Ratio, cbg)) → new_esEs19(vyw300, vyw4000, cbg)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Ratio, cge)) → new_ltEs17(vyw4310, vyw4510, cge)
new_esEs7(@2(vyw300, vyw301), @2(vyw4000, vyw4001), bff, bfg) → new_asAs(new_esEs9(vyw300, vyw4000, bff), new_esEs10(vyw301, vyw4001, bfg))
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_Maybe, ff), fb) → new_ltEs6(vyw4310, vyw4510, ff)
new_lt21(vyw4310, vyw4510, ty_Float) → new_lt11(vyw4310, vyw4510)
new_compare210(vyw430, vyw450, True) → EQ
new_esEs6(Just(vyw300), Just(vyw4000), ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs27(vyw4310, vyw4510, ty_Integer) → new_esEs16(vyw4310, vyw4510)
new_esEs23(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_ltEs4(LT, GT) → True
new_primPlusNat1(Succ(vyw770), vyw400000) → Succ(Succ(new_primPlusNat0(vyw770, vyw400000)))
new_ltEs19(vyw4311, vyw4511, ty_Char) → new_ltEs9(vyw4311, vyw4511)
new_ltEs20(vyw4312, vyw4512, app(ty_Maybe, bg)) → new_ltEs6(vyw4312, vyw4512, bg)
new_lt12(vyw430, vyw450, bfb, bfc) → new_esEs8(new_compare28(vyw430, vyw450, bfb, bfc), LT)
new_lt16(vyw430, vyw450, ty_Double) → new_lt13(vyw430, vyw450)
new_esEs25(vyw430, vyw450, ty_Integer) → new_esEs16(vyw430, vyw450)
new_primCmpInt(Neg(Zero), Neg(Succ(vyw45000))) → new_primCmpNat0(Succ(vyw45000), Zero)
new_primCmpInt(Pos(Zero), Neg(Succ(vyw45000))) → GT
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Int) → new_esEs11(vyw300, vyw4000)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Int, fb) → new_ltEs16(vyw4310, vyw4510)
new_compare13(Char(vyw4300), Char(vyw4500)) → new_primCmpNat0(vyw4300, vyw4500)
new_compare0(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bdb) → new_primCompAux1(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, bdb), bdb)
new_ltEs19(vyw4311, vyw4511, app(ty_[], bbf)) → new_ltEs7(vyw4311, vyw4511, bbf)
new_esEs27(vyw4310, vyw4510, ty_@0) → new_esEs17(vyw4310, vyw4510)
new_sr0(vyw300, vyw4000) → new_primMulInt(vyw300, vyw4000)
new_lt16(vyw430, vyw450, app(ty_[], bdb)) → new_lt9(vyw430, vyw450, bdb)
new_esEs21(vyw301, vyw4001, app(app(app(ty_@3, ccd), cce), ccf)) → new_esEs4(vyw301, vyw4001, ccd, cce, ccf)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(app(ty_@3, cfd), cfe), cff)) → new_esEs4(vyw300, vyw4000, cfd, cfe, cff)
new_lt21(vyw4310, vyw4510, ty_Ordering) → new_lt4(vyw4310, vyw4510)
new_lt16(vyw430, vyw450, app(app(ty_Either, beg), beh)) → new_lt10(vyw430, vyw450, beg, beh)
new_esEs24(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(ty_Either, cfg), cfh)) → new_esEs5(vyw300, vyw4000, cfg, cfh)
new_esEs16(Integer(vyw300), Integer(vyw4000)) → new_primEqInt(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, app(app(ty_@2, ha), hb)) → new_ltEs13(vyw4310, vyw4510, ha, hb)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(ty_@2, dag), dah), dae) → new_esEs7(vyw300, vyw4000, dag, dah)
new_lt16(vyw430, vyw450, ty_Integer) → new_lt8(vyw430, vyw450)
new_esEs21(vyw301, vyw4001, ty_Float) → new_esEs13(vyw301, vyw4001)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(ty_[], dca)) → new_esEs14(vyw300, vyw4000, dca)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_esEs25(vyw430, vyw450, ty_Bool) → new_esEs12(vyw430, vyw450)
new_ltEs4(LT, EQ) → True
new_lt19(vyw4310, vyw4510, ty_Ordering) → new_lt4(vyw4310, vyw4510)
new_primCompAux1(vyw4300, vyw4500, vyw106, bdb) → new_primCompAux0(vyw106, new_compare31(vyw4300, vyw4500, bdb))
new_lt19(vyw4310, vyw4510, ty_Bool) → new_lt14(vyw4310, vyw4510)
new_esEs20(vyw300, vyw4000, app(ty_Maybe, cbh)) → new_esEs6(vyw300, vyw4000, cbh)
new_esEs10(vyw301, vyw4001, app(app(ty_Either, bhh), caa)) → new_esEs5(vyw301, vyw4001, bhh, caa)
new_compare31(vyw4300, vyw4500, app(ty_Maybe, bdh)) → new_compare16(vyw4300, vyw4500, bdh)
new_lt20(vyw4311, vyw4511, app(ty_Maybe, db)) → new_lt7(vyw4311, vyw4511, db)
new_compare26(vyw430, vyw450, False) → new_compare17(vyw430, vyw450, new_ltEs4(vyw430, vyw450))
new_asAs(False, vyw53) → False
new_esEs29(vyw4311, vyw4511, ty_Bool) → new_esEs12(vyw4311, vyw4511)
new_compare18(vyw430, vyw450, beg, beh) → new_compare24(vyw430, vyw450, new_esEs5(vyw430, vyw450, beg, beh), beg, beh)
new_primMulInt(Neg(vyw3000), Pos(vyw40000)) → Neg(new_primMulNat0(vyw3000, vyw40000))
new_primMulInt(Pos(vyw3000), Neg(vyw40000)) → Neg(new_primMulNat0(vyw3000, vyw40000))
new_compare211(@2(vyw430, vyw431), @2(vyw450, vyw451), False, bfd, bfe) → new_compare110(vyw430, vyw431, vyw450, vyw451, new_lt16(vyw430, vyw450, bfd), new_asAs(new_esEs25(vyw430, vyw450, bfd), new_ltEs18(vyw431, vyw451, bfe)), bfd, bfe)
new_primMulNat0(Succ(vyw30000), Zero) → Zero
new_primMulNat0(Zero, Succ(vyw400000)) → Zero
new_esEs9(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs21(vyw301, vyw4001, app(app(ty_Either, ccg), cch)) → new_esEs5(vyw301, vyw4001, ccg, cch)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_Maybe, cgb)) → new_esEs6(vyw300, vyw4000, cgb)
new_esEs21(vyw301, vyw4001, ty_Ordering) → new_esEs8(vyw301, vyw4001)
new_esEs29(vyw4311, vyw4511, ty_Int) → new_esEs11(vyw4311, vyw4511)
new_esEs9(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs10(vyw301, vyw4001, app(ty_Maybe, cac)) → new_esEs6(vyw301, vyw4001, cac)
new_compare15(Double(vyw4300, vyw4301), Double(vyw4500, vyw4501)) → new_compare8(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_compare12(vyw430, vyw450, True) → LT
new_compare31(vyw4300, vyw4500, ty_Float) → new_compare19(vyw4300, vyw4500)
new_ltEs12(True, True) → True
new_compare31(vyw4300, vyw4500, app(ty_[], bec)) → new_compare0(vyw4300, vyw4500, bec)
new_ltEs18(vyw431, vyw451, app(ty_Ratio, cgg)) → new_ltEs17(vyw431, vyw451, cgg)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, ty_Double) → new_esEs15(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Float) → new_ltEs11(vyw4310, vyw4510)
new_esEs28(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, hd), he), hf)) → new_ltEs10(vyw4310, vyw4510, hd, he, hf)
new_ltEs12(False, True) → True
new_lt13(vyw430, vyw450) → new_esEs8(new_compare15(vyw430, vyw450), LT)
new_compare111(vyw86, vyw87, vyw88, vyw89, False, ddc, ddd) → GT
new_esEs10(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_ltEs18(vyw431, vyw451, app(app(ty_@2, bae), bcb)) → new_ltEs13(vyw431, vyw451, bae, bcb)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Integer) → new_ltEs8(vyw4310, vyw4510)
new_lt20(vyw4311, vyw4511, app(ty_Ratio, ddf)) → new_lt18(vyw4311, vyw4511, ddf)
new_ltEs19(vyw4311, vyw4511, ty_Int) → new_ltEs16(vyw4311, vyw4511)
new_esEs12(True, False) → False
new_esEs12(False, True) → False
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(ty_Maybe, ddb)) → new_esEs6(vyw300, vyw4000, ddb)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, eg), eh), fa), fb) → new_ltEs10(vyw4310, vyw4510, eg, eh, fa)
new_compare211(vyw43, vyw45, True, bfd, bfe) → EQ
new_ltEs6(Nothing, Nothing, cgd) → True
new_esEs27(vyw4310, vyw4510, ty_Bool) → new_esEs12(vyw4310, vyw4510)
new_esEs29(vyw4311, vyw4511, ty_Double) → new_esEs15(vyw4311, vyw4511)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_[], ga), fb) → new_ltEs7(vyw4310, vyw4510, ga)
new_compare6(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Integer) → new_compare7(new_sr(vyw4300, vyw4501), new_sr(vyw4500, vyw4301))
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_[], bad)) → new_ltEs7(vyw4310, vyw4510, bad)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_@0) → new_ltEs15(vyw4310, vyw4510)
new_ltEs4(LT, LT) → True
new_compare19(Float(vyw4300, vyw4301), Float(vyw4500, vyw4501)) → new_compare8(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_ltEs20(vyw4312, vyw4512, ty_Float) → new_ltEs11(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, app(app(ty_Either, ea), eb)) → new_lt10(vyw4310, vyw4510, ea, eb)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_Ordering) → new_ltEs4(vyw4310, vyw4510)
new_lt10(vyw430, vyw450, beg, beh) → new_esEs8(new_compare18(vyw430, vyw450, beg, beh), LT)
new_ltEs18(vyw431, vyw451, ty_Double) → new_ltEs14(vyw431, vyw451)
new_lt20(vyw4311, vyw4511, ty_Float) → new_lt11(vyw4311, vyw4511)
new_compare7(Integer(vyw4300), Integer(vyw4500)) → new_primCmpInt(vyw4300, vyw4500)
new_esEs10(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(ty_Either, dbd), dbe), dae) → new_esEs5(vyw300, vyw4000, dbd, dbe)
new_ltEs18(vyw431, vyw451, app(ty_Maybe, cgd)) → new_ltEs6(vyw431, vyw451, cgd)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Integer) → new_esEs16(vyw302, vyw4002)
new_ltEs20(vyw4312, vyw4512, ty_Integer) → new_ltEs8(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, app(app(app(ty_@3, df), dg), dh)) → new_lt15(vyw4310, vyw4510, df, dg, dh)
new_esEs26(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs29(vyw4311, vyw4511, ty_Integer) → new_esEs16(vyw4311, vyw4511)
new_esEs20(vyw300, vyw4000, app(app(ty_@2, cah), cba)) → new_esEs7(vyw300, vyw4000, cah, cba)
new_compare210(vyw430, vyw450, False) → new_compare12(vyw430, vyw450, new_ltEs12(vyw430, vyw450))
new_esEs10(vyw301, vyw4001, ty_Ordering) → new_esEs8(vyw301, vyw4001)
new_esEs5(Right(vyw300), Right(vyw4000), dbh, app(app(ty_@2, dcb), dcc)) → new_esEs7(vyw300, vyw4000, dcb, dcc)
new_lt21(vyw4310, vyw4510, ty_@0) → new_lt6(vyw4310, vyw4510)
new_lt19(vyw4310, vyw4510, ty_@0) → new_lt6(vyw4310, vyw4510)
new_primPlusNat0(Succ(vyw7700), Succ(vyw4000000)) → Succ(Succ(new_primPlusNat0(vyw7700, vyw4000000)))
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Char, fb) → new_ltEs9(vyw4310, vyw4510)
new_ltEs5(Right(vyw4310), Right(vyw4510), gb, ty_@0) → new_ltEs15(vyw4310, vyw4510)
new_compare0([], :(vyw4500, vyw4501), bdb) → LT
new_esEs27(vyw4310, vyw4510, app(ty_[], bch)) → new_esEs14(vyw4310, vyw4510, bch)
new_esEs9(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs14(:(vyw300, vyw301), :(vyw4000, vyw4001), cgh) → new_asAs(new_esEs26(vyw300, vyw4000, cgh), new_esEs14(vyw301, vyw4001, cgh))
new_compare31(vyw4300, vyw4500, ty_Char) → new_compare13(vyw4300, vyw4500)
new_asAs(True, vyw53) → vyw53
new_esEs25(vyw430, vyw450, ty_Int) → new_esEs11(vyw430, vyw450)
new_esEs20(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs26(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Ordering) → new_ltEs4(vyw4310, vyw4510)
new_compare17(vyw430, vyw450, False) → GT
new_compare27(vyw430, vyw450, True, bed, bee, bef) → EQ
new_ltEs20(vyw4312, vyw4512, app(app(app(ty_@3, bb), bc), bd)) → new_ltEs10(vyw4312, vyw4512, bb, bc, bd)
new_esEs20(vyw300, vyw4000, app(ty_[], cag)) → new_esEs14(vyw300, vyw4000, cag)
new_esEs9(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_ltEs20(vyw4312, vyw4512, app(app(ty_@2, bh), ca)) → new_ltEs13(vyw4312, vyw4512, bh, ca)
new_ltEs7(vyw431, vyw451, bda) → new_not(new_esEs8(new_compare0(vyw431, vyw451, bda), GT))
new_ltEs19(vyw4311, vyw4511, app(app(app(ty_@3, baf), bag), bah)) → new_ltEs10(vyw4311, vyw4511, baf, bag, bah)
new_esEs27(vyw4310, vyw4510, ty_Char) → new_esEs18(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, app(ty_Ratio, daa)) → new_esEs19(vyw300, vyw4000, daa)
new_ltEs4(GT, GT) → True
new_compare30(vyw430, vyw450, bed, bee, bef) → new_compare27(vyw430, vyw450, new_esEs4(vyw430, vyw450, bed, bee, bef), bed, bee, bef)
new_esEs28(vyw4310, vyw4510, ty_Char) → new_esEs18(vyw4310, vyw4510)
new_compare25(vyw430, vyw450, False, bfa) → new_compare11(vyw430, vyw450, new_ltEs6(vyw430, vyw450, bfa), bfa)
new_esEs21(vyw301, vyw4001, ty_Bool) → new_esEs12(vyw301, vyw4001)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, app(app(ty_Either, cea), ceb)) → new_esEs5(vyw302, vyw4002, cea, ceb)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_primCompAux0(vyw114, EQ) → vyw114
new_esEs29(vyw4311, vyw4511, ty_Ordering) → new_esEs8(vyw4311, vyw4511)
new_ltEs20(vyw4312, vyw4512, app(app(ty_Either, be), bf)) → new_ltEs5(vyw4312, vyw4512, be, bf)
new_ltEs18(vyw431, vyw451, ty_Integer) → new_ltEs8(vyw431, vyw451)
new_esEs28(vyw4310, vyw4510, ty_Bool) → new_esEs12(vyw4310, vyw4510)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primCmpInt(Neg(Succ(vyw43000)), Pos(vyw4500)) → LT
new_compare6(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Int) → new_compare8(new_sr0(vyw4300, vyw4501), new_sr0(vyw4500, vyw4301))
new_not(True) → False

The set Q consists of the following terms:

new_compare15(Double(x0, x1), Double(x2, x3))
new_sr0(x0, x1)
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), Succ(x1))
new_ltEs20(x0, x1, ty_Float)
new_esEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_lt20(x0, x1, ty_Double)
new_esEs28(x0, x1, ty_Ordering)
new_esEs5(Right(x0), Right(x1), x2, ty_Float)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_compare31(x0, x1, ty_Double)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Zero)
new_compare24(x0, x1, False, x2, x3)
new_esEs12(False, False)
new_esEs11(x0, x1)
new_esEs28(x0, x1, ty_Double)
new_ltEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Int)
new_lt21(x0, x1, ty_Ordering)
new_compare31(x0, x1, ty_Float)
new_lt19(x0, x1, app(ty_Maybe, x2))
new_compare12(x0, x1, False)
new_ltEs19(x0, x1, ty_Char)
new_lt19(x0, x1, ty_Ordering)
new_esEs29(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare31(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_compare16(x0, x1, x2)
new_esEs16(Integer(x0), Integer(x1))
new_esEs26(x0, x1, ty_Double)
new_lt21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs5(Left(x0), Left(x1), ty_Double, x2)
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_lt16(x0, x1, ty_Float)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs8(GT, GT)
new_compare14(x0, x1, True, x2, x3, x4)
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_asAs(True, x0)
new_esEs5(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Nothing, Just(x0), x1)
new_esEs6(Just(x0), Nothing, x1)
new_esEs5(Left(x0), Left(x1), ty_Int, x2)
new_ltEs5(Right(x0), Right(x1), x2, ty_Float)
new_compare31(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Bool)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_lt21(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs8(LT, LT)
new_ltEs20(x0, x1, ty_Integer)
new_esEs14(:(x0, x1), [], x2)
new_esEs26(x0, x1, ty_Ordering)
new_ltEs8(x0, x1)
new_esEs5(Left(x0), Left(x1), ty_Integer, x2)
new_esEs29(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_compare11(x0, x1, True, x2)
new_lt13(x0, x1)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_compare27(x0, x1, True, x2, x3, x4)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_lt10(x0, x1, x2, x3)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs10(x0, x1, ty_Float)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs9(x0, x1, app(ty_[], x2))
new_compare17(x0, x1, False)
new_ltEs19(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primCompAux0(x0, EQ)
new_esEs26(x0, x1, app(ty_[], x2))
new_compare26(x0, x1, True)
new_esEs5(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primEqNat0(Zero, Zero)
new_ltEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs29(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Double)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_lt21(x0, x1, ty_Int)
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_lt6(x0, x1)
new_lt20(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_ltEs18(x0, x1, ty_Integer)
new_lt16(x0, x1, app(app(ty_@2, x2), x3))
new_esEs29(x0, x1, ty_Integer)
new_compare31(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Succ(x0), Zero)
new_compare31(x0, x1, ty_Integer)
new_compare6(:%(x0, x1), :%(x2, x3), ty_Integer)
new_ltEs5(Left(x0), Right(x1), x2, x3)
new_ltEs5(Right(x0), Left(x1), x2, x3)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Int)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Succ(x0), x1)
new_compare11(x0, x1, False, x2)
new_compare13(Char(x0), Char(x1))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Zero, Succ(x0))
new_primMulNat0(Zero, Zero)
new_compare18(x0, x1, x2, x3)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_ltEs5(Right(x0), Right(x1), x2, ty_@0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_sr(Integer(x0), Integer(x1))
new_esEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_Int)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_ltEs5(Right(x0), Right(x1), x2, ty_Integer)
new_compare0([], [], x0)
new_ltEs4(GT, GT)
new_esEs28(x0, x1, ty_@0)
new_lt19(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_ltEs19(x0, x1, ty_Ordering)
new_esEs14([], :(x0, x1), x2)
new_esEs28(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs10(x0, x1, ty_Integer)
new_esEs10(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Bool)
new_lt16(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, ty_Ordering)
new_ltEs5(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_lt20(x0, x1, app(ty_[], x2))
new_lt19(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, ty_Integer)
new_primMulNat0(Succ(x0), Succ(x1))
new_ltEs16(x0, x1)
new_compare31(x0, x1, app(ty_[], x2))
new_primCompAux1(x0, x1, x2, x3)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_lt19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs12(False, False)
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Integer)
new_compare26(x0, x1, False)
new_ltEs19(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), ty_Float, x2)
new_lt21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_lt9(x0, x1, x2)
new_lt21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs29(x0, x1, ty_Double)
new_compare31(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs28(x0, x1, ty_Float)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs5(Left(x0), Left(x1), ty_Bool, x2)
new_esEs25(x0, x1, ty_Ordering)
new_ltEs5(Right(x0), Right(x1), x2, ty_Int)
new_lt19(x0, x1, ty_Integer)
new_primPlusNat1(Zero, x0)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_compare24(x0, x1, True, x2, x3)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Bool)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, ty_Float)
new_lt16(x0, x1, app(ty_Ratio, x2))
new_primPlusNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Bool)
new_lt16(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_compare8(x0, x1)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, ty_Char)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_compare31(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Integer)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_primCompAux0(x0, LT)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_ltEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_ltEs4(EQ, EQ)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt21(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_ltEs19(x0, x1, ty_Double)
new_esEs17(@0, @0)
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_compare25(x0, x1, False, x2)
new_ltEs18(x0, x1, app(app(ty_@2, x2), x3))
new_compare210(x0, x1, False)
new_esEs5(Left(x0), Left(x1), ty_@0, x2)
new_esEs28(x0, x1, ty_Integer)
new_esEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_ltEs4(LT, EQ)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_ltEs4(EQ, LT)
new_compare29(x0, x1)
new_ltEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_compare27(x0, x1, False, x2, x3, x4)
new_esEs5(Left(x0), Left(x1), ty_Float, x2)
new_esEs12(True, True)
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_lt19(x0, x1, app(app(ty_@2, x2), x3))
new_lt21(x0, x1, app(ty_Maybe, x2))
new_compare0([], :(x0, x1), x2)
new_lt16(x0, x1, ty_@0)
new_pePe(True, x0)
new_esEs22(x0, x1, ty_@0)
new_ltEs18(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Integer)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_lt20(x0, x1, ty_Bool)
new_esEs6(Nothing, Nothing, x0)
new_ltEs6(Just(x0), Nothing, x1)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_ltEs20(x0, x1, ty_Char)
new_ltEs19(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_ltEs18(x0, x1, app(ty_[], x2))
new_esEs5(Left(x0), Left(x1), ty_Double, x2)
new_ltEs5(Left(x0), Left(x1), ty_Char, x2)
new_pePe(False, x0)
new_ltEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_lt21(x0, x1, ty_Double)
new_esEs5(Right(x0), Right(x1), x2, ty_Char)
new_compare110(x0, x1, x2, x3, True, x4, x5, x6)
new_ltEs18(x0, x1, ty_Double)
new_compare12(x0, x1, True)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Double)
new_ltEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Ordering)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs8(EQ, EQ)
new_esEs29(x0, x1, app(app(ty_Either, x2), x3))
new_compare25(x0, x1, True, x2)
new_primCmpNat0(Zero, Succ(x0))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_lt7(x0, x1, x2)
new_esEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_lt5(x0, x1)
new_esEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs24(x0, x1, ty_Integer)
new_compare110(x0, x1, x2, x3, False, x4, x5, x6)
new_esEs5(Right(x0), Right(x1), x2, ty_Int)
new_primEqInt(Neg(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_lt8(x0, x1)
new_asAs(False, x0)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_lt15(x0, x1, x2, x3, x4)
new_ltEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_ltEs4(LT, LT)
new_esEs27(x0, x1, ty_Double)
new_lt16(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_lt19(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Integer)
new_esEs5(Right(x0), Left(x1), x2, x3)
new_esEs5(Left(x0), Right(x1), x2, x3)
new_primCmpNat0(Succ(x0), Zero)
new_compare211(@2(x0, x1), @2(x2, x3), False, x4, x5)
new_lt16(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, False, x2, x3)
new_esEs29(x0, x1, app(ty_Maybe, x2))
new_lt20(x0, x1, ty_Char)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_lt14(x0, x1)
new_esEs10(x0, x1, ty_Int)
new_ltEs14(x0, x1)
new_compare31(x0, x1, ty_Ordering)
new_ltEs5(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs19(x0, x1, ty_Bool)
new_ltEs20(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_ltEs12(False, True)
new_ltEs12(True, False)
new_esEs25(x0, x1, ty_Int)
new_lt18(x0, x1, x2)
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_compare31(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_primCmpNat0(Zero, Zero)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_lt19(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_lt16(x0, x1, ty_Char)
new_ltEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_ltEs18(x0, x1, ty_Bool)
new_ltEs17(x0, x1, x2)
new_ltEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs29(x0, x1, ty_@0)
new_compare17(x0, x1, True)
new_lt19(x0, x1, ty_Char)
new_compare210(x0, x1, True)
new_ltEs9(x0, x1)
new_ltEs5(Left(x0), Left(x1), ty_@0, x2)
new_primMulInt(Neg(x0), Neg(x1))
new_ltEs15(x0, x1)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_compare31(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs29(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Char)
new_esEs29(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, ty_Float)
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(True, False)
new_esEs12(False, True)
new_ltEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_ltEs11(x0, x1)
new_esEs21(x0, x1, ty_@0)
new_compare9(@0, @0)
new_esEs5(Right(x0), Right(x1), x2, ty_Bool)
new_esEs29(x0, x1, ty_Bool)
new_esEs15(Double(x0, x1), Double(x2, x3))
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Ordering)
new_compare10(x0, x1, True, x2, x3)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt4(x0, x1)
new_ltEs4(EQ, GT)
new_ltEs4(GT, EQ)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_not(True)
new_ltEs5(Right(x0), Right(x1), x2, ty_Char)
new_esEs18(Char(x0), Char(x1))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_compare211(x0, x1, True, x2, x3)
new_lt19(x0, x1, app(ty_Ratio, x2))
new_lt16(x0, x1, ty_Ordering)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_primMulInt(Pos(x0), Pos(x1))
new_esEs28(x0, x1, ty_Int)
new_not(False)
new_ltEs18(x0, x1, ty_Char)
new_primCmpNat0(Succ(x0), Succ(x1))
new_ltEs18(x0, x1, ty_@0)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_ltEs18(x0, x1, app(ty_Maybe, x2))
new_compare0(:(x0, x1), [], x2)
new_ltEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_ltEs12(True, True)
new_ltEs5(Left(x0), Left(x1), ty_Integer, x2)
new_esEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs20(x0, x1, app(ty_[], x2))
new_compare5(x0, x1)
new_esEs26(x0, x1, ty_@0)
new_esEs5(Left(x0), Left(x1), ty_Char, x2)
new_compare19(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_@0)
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_ltEs20(x0, x1, app(ty_[], x2))
new_compare111(x0, x1, x2, x3, False, x4, x5)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_ltEs18(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs5(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs29(x0, x1, ty_Int)
new_ltEs7(x0, x1, x2)
new_esEs29(x0, x1, app(ty_[], x2))
new_compare0(:(x0, x1), :(x2, x3), x4)
new_esEs29(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs9(x0, x1, ty_Double)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_lt19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, ty_Double)
new_ltEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_esEs26(x0, x1, ty_Int)
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_compare30(x0, x1, x2, x3, x4)
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, ty_Int)
new_ltEs18(x0, x1, app(ty_Ratio, x2))
new_lt20(x0, x1, ty_Float)
new_compare28(x0, x1, x2, x3)
new_esEs10(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Bool)
new_lt21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_compare14(x0, x1, False, x2, x3, x4)
new_compare31(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Succ(x1))
new_primCompAux0(x0, GT)
new_lt17(x0, x1)
new_esEs20(x0, x1, ty_Bool)
new_lt16(x0, x1, app(ty_Maybe, x2))
new_compare31(x0, x1, ty_Bool)
new_compare6(:%(x0, x1), :%(x2, x3), ty_Int)
new_lt19(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs9(x0, x1, ty_Bool)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_compare111(x0, x1, x2, x3, True, x4, x5)
new_esEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(x0, x1, ty_@0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_compare7(Integer(x0), Integer(x1))
new_ltEs19(x0, x1, app(ty_[], x2))
new_lt21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, app(ty_Maybe, x2))
new_lt16(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_@0)
new_lt21(x0, x1, ty_Bool)
new_esEs14([], [], x0)
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_lt21(x0, x1, ty_@0)
new_ltEs4(GT, LT)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs4(LT, GT)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_lt20(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Ordering)
new_primPlusNat0(Zero, Succ(x0))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt11(x0, x1)
new_lt16(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs25(x0, x1, ty_Double)
new_lt12(x0, x1, x2, x3)
new_ltEs6(Nothing, Just(x0), x1)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_lt21(x0, x1, ty_Float)
new_ltEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs27(x0, x1, app(ty_[], x2))
new_lt16(x0, x1, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_elemFM0(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, False, h, ba, bb) → new_elemFM00(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, new_esEs8(new_compare211(@2(vyw21, vyw22), @2(vyw15, vyw16), new_esEs7(@2(vyw21, vyw22), @2(vyw15, vyw16), ba, bb), ba, bb), GT), h, ba, bb)
new_elemFM0(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, True, h, ba, bb) → new_elemFM01(vyw19, @2(vyw21, vyw22), h, ba, bb)
new_elemFM00(vyw15, vyw16, vyw17, vyw18, vyw19, vyw20, vyw21, vyw22, True, h, ba, bb) → new_elemFM01(vyw20, @2(vyw21, vyw22), h, ba, bb)
new_elemFM01(Branch(@2(vyw400, vyw401), vyw41, vyw42, vyw43, vyw44), @2(vyw30, vyw31), bc, bd, be) → new_elemFM0(vyw400, vyw401, vyw41, vyw42, vyw43, vyw44, vyw30, vyw31, new_esEs30(vyw30, vyw31, vyw400, vyw401, new_esEs31(vyw30, vyw400, bd), bd, be), bc, bd, be)

The TRS R consists of the following rules:

new_esEs25(vyw430, vyw450, app(ty_[], bfh)) → new_esEs14(vyw430, vyw450, bfh)
new_esEs19(:%(vyw300, vyw301), :%(vyw4000, vyw4001), bgc) → new_asAs(new_esEs23(vyw300, vyw4000, bgc), new_esEs24(vyw301, vyw4001, bgc))
new_lt4(vyw430, vyw450) → new_esEs8(new_compare5(vyw430, vyw450), LT)
new_compare31(vyw4300, vyw4500, ty_Double) → new_compare15(vyw4300, vyw4500)
new_lt16(vyw430, vyw450, ty_Int) → new_lt5(vyw430, vyw450)
new_esEs18(Char(vyw300), Char(vyw4000)) → new_primEqNat0(vyw300, vyw4000)
new_lt19(vyw4310, vyw4510, app(app(ty_Either, cfc), cfd)) → new_lt10(vyw4310, vyw4510, cfc, cfd)
new_esEs10(vyw301, vyw4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs4(vyw301, vyw4001, df, dg, dh)
new_ltEs4(EQ, GT) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(ty_Maybe, beh)) → new_ltEs6(vyw4310, vyw4510, beh)
new_esEs20(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs31(vyw30, vyw400, ty_Ordering) → new_esEs8(vyw30, vyw400)
new_compare10(vyw430, vyw450, True, ee, ef) → LT
new_ltEs13(@2(vyw4310, vyw4311), @2(vyw4510, vyw4511), cdb, cdc) → new_pePe(new_lt19(vyw4310, vyw4510, cdb), new_asAs(new_esEs27(vyw4310, vyw4510, cdb), new_ltEs19(vyw4311, vyw4511, cdc)))
new_esEs20(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_lt21(vyw4310, vyw4510, app(ty_Maybe, dda)) → new_lt7(vyw4310, vyw4510, dda)
new_ltEs19(vyw4311, vyw4511, ty_Float) → new_ltEs11(vyw4311, vyw4511)
new_ltEs6(Nothing, Just(vyw4510), cba) → True
new_ltEs20(vyw4312, vyw4512, app(ty_[], dga)) → new_ltEs7(vyw4312, vyw4512, dga)
new_compare14(vyw430, vyw450, True, bfe, bff, bfg) → LT
new_esEs31(vyw30, vyw400, app(ty_[], cde)) → new_esEs14(vyw30, vyw400, cde)
new_compare31(vyw4300, vyw4500, ty_Int) → new_compare8(vyw4300, vyw4500)
new_esEs31(vyw30, vyw400, ty_@0) → new_esEs17(vyw30, vyw400)
new_lt20(vyw4311, vyw4511, ty_@0) → new_lt6(vyw4311, vyw4511)
new_esEs26(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_ltEs9(vyw431, vyw451) → new_not(new_esEs8(new_compare13(vyw431, vyw451), GT))
new_esEs21(vyw301, vyw4001, ty_@0) → new_esEs17(vyw301, vyw4001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(vyw4310, vyw4510, app(ty_Ratio, cfh)) → new_esEs19(vyw4310, vyw4510, cfh)
new_ltEs20(vyw4312, vyw4512, ty_@0) → new_ltEs15(vyw4312, vyw4512)
new_esEs27(vyw4310, vyw4510, app(app(app(ty_@3, ceh), cfa), cfb)) → new_esEs4(vyw4310, vyw4510, ceh, cfa, cfb)
new_sr(Integer(vyw43000), Integer(vyw45010)) → Integer(new_primMulInt(vyw43000, vyw45010))
new_esEs12(True, True) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_@0, bdb) → new_ltEs15(vyw4310, vyw4510)
new_esEs30(vyw31, vyw32, vyw33, vyw34, True, bbc, bbd) → new_esEs8(new_compare211(@2(vyw31, vyw32), @2(vyw33, vyw34), new_esEs32(vyw32, vyw34, bbd), bbc, bbd), LT)
new_compare25(vyw430, vyw450, True, eg) → EQ
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Ordering, bdb) → new_ltEs4(vyw4310, vyw4510)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_@0) → new_esEs17(vyw302, vyw4002)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_Ratio, dae), chd) → new_esEs19(vyw300, vyw4000, dae)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Bool, chd) → new_esEs12(vyw300, vyw4000)
new_ltEs8(vyw431, vyw451) → new_not(new_esEs8(new_compare7(vyw431, vyw451), GT))
new_esEs22(vyw302, vyw4002, app(ty_Ratio, bba)) → new_esEs19(vyw302, vyw4002, bba)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(ty_@2, bdf), bdg), bdb) → new_ltEs13(vyw4310, vyw4510, bdf, bdg)
new_esEs4(@3(vyw300, vyw301, vyw302), @3(vyw4000, vyw4001, vyw4002), fa, fb, fc) → new_asAs(new_esEs20(vyw300, vyw4000, fa), new_asAs(new_esEs21(vyw301, vyw4001, fb), new_esEs22(vyw302, vyw4002, fc)))
new_compare5(vyw430, vyw450) → new_compare26(vyw430, vyw450, new_esEs8(vyw430, vyw450))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Float) → new_ltEs11(vyw4310, vyw4510)
new_ltEs5(Left(vyw4310), Right(vyw4510), beb, bdb) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(ty_Ratio, bfc)) → new_ltEs17(vyw4310, vyw4510, bfc)
new_lt17(vyw430, vyw450) → new_esEs8(new_compare13(vyw430, vyw450), LT)
new_esEs22(vyw302, vyw4002, app(ty_Maybe, bbb)) → new_esEs6(vyw302, vyw4002, bbb)
new_lt9(vyw430, vyw450, bfh) → new_esEs8(new_compare0(vyw430, vyw450, bfh), LT)
new_esEs27(vyw4310, vyw4510, app(ty_Maybe, cfe)) → new_esEs6(vyw4310, vyw4510, cfe)
new_lt16(vyw430, vyw450, ty_Char) → new_lt17(vyw430, vyw450)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(ty_@2, bgf), bgg)) → new_esEs7(vyw300, vyw4000, bgf, bgg)
new_esEs29(vyw4311, vyw4511, app(ty_Ratio, def)) → new_esEs19(vyw4311, vyw4511, def)
new_esEs25(vyw430, vyw450, ty_Double) → new_esEs15(vyw430, vyw450)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(app(ty_@3, chh), daa), dab), chd) → new_esEs4(vyw300, vyw4000, chh, daa, dab)
new_compare31(vyw4300, vyw4500, app(app(app(ty_@3, bhg), bhh), caa)) → new_compare30(vyw4300, vyw4500, bhg, bhh, caa)
new_compare110(vyw86, vyw87, vyw88, vyw89, True, vyw91, dcb, dcc) → new_compare111(vyw86, vyw87, vyw88, vyw89, True, dcb, dcc)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(app(ty_Either, bef), beg)) → new_ltEs5(vyw4310, vyw4510, bef, beg)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, app(ty_[], baa)) → new_esEs14(vyw302, vyw4002, baa)
new_ltEs18(vyw431, vyw451, app(ty_[], eh)) → new_ltEs7(vyw431, vyw451, eh)
new_compare29(vyw430, vyw450) → new_compare210(vyw430, vyw450, new_esEs12(vyw430, vyw450))
new_ltEs5(Right(vyw4310), Left(vyw4510), beb, bdb) → False
new_lt20(vyw4311, vyw4511, ty_Bool) → new_lt14(vyw4311, vyw4511)
new_esEs17(@0, @0) → True
new_lt21(vyw4310, vyw4510, app(app(ty_@2, ddb), ddc)) → new_lt12(vyw4310, vyw4510, ddb, ddc)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_@2, cbh), cca)) → new_ltEs13(vyw4310, vyw4510, cbh, cca)
new_esEs25(vyw430, vyw450, ty_Float) → new_esEs13(vyw430, vyw450)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_Ratio, bdh), bdb) → new_ltEs17(vyw4310, vyw4510, bdh)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_Maybe, daf), chd) → new_esEs6(vyw300, vyw4000, daf)
new_esEs32(vyw32, vyw34, app(ty_[], bbe)) → new_esEs14(vyw32, vyw34, bbe)
new_pePe(False, vyw105) → vyw105
new_esEs14([], [], cde) → True
new_esEs25(vyw430, vyw450, app(app(ty_@2, bga), bgb)) → new_esEs7(vyw430, vyw450, bga, bgb)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Integer, bdb) → new_ltEs8(vyw4310, vyw4510)
new_lt7(vyw430, vyw450, eg) → new_esEs8(new_compare16(vyw430, vyw450, eg), LT)
new_esEs31(vyw30, vyw400, app(app(app(ty_@3, fa), fb), fc)) → new_esEs4(vyw30, vyw400, fa, fb, fc)
new_ltEs12(True, False) → False
new_esEs10(vyw301, vyw4001, ty_Bool) → new_esEs12(vyw301, vyw4001)
new_esEs29(vyw4311, vyw4511, ty_Char) → new_esEs18(vyw4311, vyw4511)
new_esEs29(vyw4311, vyw4511, app(ty_[], deg)) → new_esEs14(vyw4311, vyw4511, deg)
new_lt19(vyw4310, vyw4510, app(ty_Maybe, cfe)) → new_lt7(vyw4310, vyw4510, cfe)
new_lt6(vyw430, vyw450) → new_esEs8(new_compare9(vyw430, vyw450), LT)
new_lt18(vyw430, vyw450, ccf) → new_esEs8(new_compare6(vyw430, vyw450, ccf), LT)
new_esEs29(vyw4311, vyw4511, ty_@0) → new_esEs17(vyw4311, vyw4511)
new_compare31(vyw4300, vyw4500, ty_Bool) → new_compare29(vyw4300, vyw4500)
new_lt19(vyw4310, vyw4510, app(ty_[], cga)) → new_lt9(vyw4310, vyw4510, cga)
new_lt21(vyw4310, vyw4510, app(ty_Ratio, ddd)) → new_lt18(vyw4310, vyw4510, ddd)
new_compare27(vyw430, vyw450, False, bfe, bff, bfg) → new_compare14(vyw430, vyw450, new_ltEs10(vyw430, vyw450, bfe, bff, bfg), bfe, bff, bfg)
new_esEs26(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Double) → new_esEs15(vyw302, vyw4002)
new_esEs26(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Int) → new_esEs11(vyw302, vyw4002)
new_esEs21(vyw301, vyw4001, app(ty_Ratio, hg)) → new_esEs19(vyw301, vyw4001, hg)
new_esEs28(vyw4310, vyw4510, app(app(app(ty_@3, dcd), dce), dcf)) → new_esEs4(vyw4310, vyw4510, dcd, dce, dcf)
new_lt16(vyw430, vyw450, ty_Bool) → new_lt14(vyw430, vyw450)
new_esEs21(vyw301, vyw4001, ty_Double) → new_esEs15(vyw301, vyw4001)
new_ltEs18(vyw431, vyw451, ty_Int) → new_ltEs16(vyw431, vyw451)
new_esEs22(vyw302, vyw4002, ty_Ordering) → new_esEs8(vyw302, vyw4002)
new_esEs32(vyw32, vyw34, ty_Integer) → new_esEs16(vyw32, vyw34)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Int, chd) → new_esEs11(vyw300, vyw4000)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Ordering, chd) → new_esEs8(vyw300, vyw4000)
new_ltEs10(@3(vyw4310, vyw4311, vyw4312), @3(vyw4510, vyw4511, vyw4512), ccg, cch, cda) → new_pePe(new_lt21(vyw4310, vyw4510, ccg), new_asAs(new_esEs28(vyw4310, vyw4510, ccg), new_pePe(new_lt20(vyw4311, vyw4511, cch), new_asAs(new_esEs29(vyw4311, vyw4511, cch), new_ltEs20(vyw4312, vyw4512, cda)))))
new_lt19(vyw4310, vyw4510, ty_Int) → new_lt5(vyw4310, vyw4510)
new_primCmpNat0(Zero, Succ(vyw45000)) → LT
new_ltEs20(vyw4312, vyw4512, ty_Double) → new_ltEs14(vyw4312, vyw4512)
new_esEs9(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs25(vyw430, vyw450, app(app(ty_Either, ee), ef)) → new_esEs5(vyw430, vyw450, ee, ef)
new_esEs8(LT, LT) → True
new_lt16(vyw430, vyw450, ty_Ordering) → new_lt4(vyw430, vyw450)
new_esEs31(vyw30, vyw400, ty_Double) → new_esEs15(vyw30, vyw400)
new_lt20(vyw4311, vyw4511, ty_Int) → new_lt5(vyw4311, vyw4511)
new_esEs25(vyw430, vyw450, ty_Ordering) → new_esEs8(vyw430, vyw450)
new_esEs29(vyw4311, vyw4511, app(app(ty_@2, ded), dee)) → new_esEs7(vyw4311, vyw4511, ded, dee)
new_esEs28(vyw4310, vyw4510, ty_Double) → new_esEs15(vyw4310, vyw4510)
new_esEs28(vyw4310, vyw4510, ty_Integer) → new_esEs16(vyw4310, vyw4510)
new_lt11(vyw430, vyw450) → new_esEs8(new_compare19(vyw430, vyw450), LT)
new_esEs10(vyw301, vyw4001, app(ty_Ratio, ec)) → new_esEs19(vyw301, vyw4001, ec)
new_pePe(True, vyw105) → True
new_compare0([], [], bfh) → EQ
new_primEqNat0(Zero, Zero) → True
new_compare31(vyw4300, vyw4500, app(app(ty_Either, cab), cac)) → new_compare18(vyw4300, vyw4500, cab, cac)
new_esEs20(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_compare26(vyw430, vyw450, True) → EQ
new_compare31(vyw4300, vyw4500, app(ty_Ratio, cag)) → new_compare6(vyw4300, vyw4500, cag)
new_esEs29(vyw4311, vyw4511, app(ty_Maybe, dec)) → new_esEs6(vyw4311, vyw4511, dec)
new_ltEs12(False, False) → True
new_ltEs20(vyw4312, vyw4512, ty_Ordering) → new_ltEs4(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, ty_Bool) → new_lt14(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, app(ty_Maybe, ceg)) → new_esEs6(vyw300, vyw4000, ceg)
new_compare11(vyw430, vyw450, True, eg) → LT
new_primMulNat0(Succ(vyw30000), Succ(vyw400000)) → new_primPlusNat1(new_primMulNat0(vyw30000, Succ(vyw400000)), vyw400000)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Char) → new_ltEs9(vyw4310, vyw4510)
new_esEs32(vyw32, vyw34, ty_Double) → new_esEs15(vyw32, vyw34)
new_ltEs18(vyw431, vyw451, ty_Char) → new_ltEs9(vyw431, vyw451)
new_lt20(vyw4311, vyw4511, app(ty_[], deg)) → new_lt9(vyw4311, vyw4511, deg)
new_esEs9(vyw300, vyw4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs4(vyw300, vyw4000, cc, cd, ce)
new_esEs22(vyw302, vyw4002, app(app(ty_@2, bab), bac)) → new_esEs7(vyw302, vyw4002, bab, bac)
new_esEs9(vyw300, vyw4000, app(ty_Maybe, db)) → new_esEs6(vyw300, vyw4000, db)
new_esEs32(vyw32, vyw34, ty_Bool) → new_esEs12(vyw32, vyw34)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Float) → new_esEs13(vyw300, vyw4000)
new_ltEs18(vyw431, vyw451, app(app(app(ty_@3, ccg), cch), cda)) → new_ltEs10(vyw431, vyw451, ccg, cch, cda)
new_lt19(vyw4310, vyw4510, ty_Double) → new_lt13(vyw4310, vyw4510)
new_esEs6(Just(vyw300), Just(vyw4000), ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs32(vyw32, vyw34, app(app(ty_@2, bbf), bbg)) → new_esEs7(vyw32, vyw34, bbf, bbg)
new_esEs26(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs8(GT, GT) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Bool, bdb) → new_ltEs12(vyw4310, vyw4510)
new_esEs12(False, False) → True
new_ltEs19(vyw4311, vyw4511, ty_Bool) → new_ltEs12(vyw4311, vyw4511)
new_esEs26(vyw300, vyw4000, app(app(app(ty_@3, cea), ceb), cec)) → new_esEs4(vyw300, vyw4000, cea, ceb, cec)
new_ltEs18(vyw431, vyw451, app(app(ty_Either, beb), bdb)) → new_ltEs5(vyw431, vyw451, beb, bdb)
new_compare110(vyw86, vyw87, vyw88, vyw89, False, vyw91, dcb, dcc) → new_compare111(vyw86, vyw87, vyw88, vyw89, vyw91, dcb, dcc)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_lt20(vyw4311, vyw4511, ty_Char) → new_lt17(vyw4311, vyw4511)
new_lt19(vyw4310, vyw4510, app(app(app(ty_@3, ceh), cfa), cfb)) → new_lt15(vyw4310, vyw4510, ceh, cfa, cfb)
new_ltEs20(vyw4312, vyw4512, ty_Int) → new_ltEs16(vyw4312, vyw4512)
new_esEs13(Float(vyw300, vyw301), Float(vyw4000, vyw4001)) → new_esEs11(new_sr0(vyw300, vyw4000), new_sr0(vyw301, vyw4001))
new_primEqInt(Neg(Succ(vyw3000)), Neg(Succ(vyw40000))) → new_primEqNat0(vyw3000, vyw40000)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Char) → new_ltEs9(vyw4310, vyw4510)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Integer, chd) → new_esEs16(vyw300, vyw4000)
new_ltEs19(vyw4311, vyw4511, ty_Integer) → new_ltEs8(vyw4311, vyw4511)
new_esEs20(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_ltEs20(vyw4312, vyw4512, ty_Char) → new_ltEs9(vyw4312, vyw4512)
new_esEs9(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Double) → new_ltEs14(vyw4310, vyw4510)
new_ltEs19(vyw4311, vyw4511, app(ty_Ratio, chb)) → new_ltEs17(vyw4311, vyw4511, chb)
new_esEs5(Left(vyw300), Left(vyw4000), app(ty_[], che), chd) → new_esEs14(vyw300, vyw4000, che)
new_esEs28(vyw4310, vyw4510, ty_@0) → new_esEs17(vyw4310, vyw4510)
new_ltEs20(vyw4312, vyw4512, ty_Bool) → new_ltEs12(vyw4312, vyw4512)
new_lt16(vyw430, vyw450, app(ty_Maybe, eg)) → new_lt7(vyw430, vyw450, eg)
new_esEs32(vyw32, vyw34, app(ty_Ratio, bce)) → new_esEs19(vyw32, vyw34, bce)
new_esEs29(vyw4311, vyw4511, app(app(ty_Either, dea), deb)) → new_esEs5(vyw4311, vyw4511, dea, deb)
new_esEs31(vyw30, vyw400, app(ty_Ratio, bgc)) → new_esEs19(vyw30, vyw400, bgc)
new_compare28(vyw430, vyw450, bga, bgb) → new_compare211(vyw430, vyw450, new_esEs7(vyw430, vyw450, bga, bgb), bga, bgb)
new_esEs14([], :(vyw4000, vyw4001), cde) → False
new_esEs14(:(vyw300, vyw301), [], cde) → False
new_esEs9(vyw300, vyw4000, app(ty_[], bh)) → new_esEs14(vyw300, vyw4000, bh)
new_compare111(vyw86, vyw87, vyw88, vyw89, True, dcb, dcc) → LT
new_esEs25(vyw430, vyw450, ty_Char) → new_esEs18(vyw430, vyw450)
new_compare31(vyw4300, vyw4500, ty_Integer) → new_compare7(vyw4300, vyw4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs19(vyw4311, vyw4511, ty_Ordering) → new_ltEs4(vyw4311, vyw4511)
new_esEs21(vyw301, vyw4001, app(app(ty_@2, gh), ha)) → new_esEs7(vyw301, vyw4001, gh, ha)
new_lt15(vyw430, vyw450, bfe, bff, bfg) → new_esEs8(new_compare30(vyw430, vyw450, bfe, bff, bfg), LT)
new_esEs20(vyw300, vyw4000, ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs27(vyw4310, vyw4510, app(app(ty_Either, cfc), cfd)) → new_esEs5(vyw4310, vyw4510, cfc, cfd)
new_lt16(vyw430, vyw450, app(ty_Ratio, ccf)) → new_lt18(vyw430, vyw450, ccf)
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(ty_Ratio, dbh)) → new_esEs19(vyw300, vyw4000, dbh)
new_ltEs20(vyw4312, vyw4512, app(ty_Ratio, dfh)) → new_ltEs17(vyw4312, vyw4512, dfh)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Float) → new_esEs13(vyw300, vyw4000)
new_esEs26(vyw300, vyw4000, app(ty_[], cdf)) → new_esEs14(vyw300, vyw4000, cdf)
new_esEs9(vyw300, vyw4000, app(ty_Ratio, da)) → new_esEs19(vyw300, vyw4000, da)
new_compare8(vyw430, vyw450) → new_primCmpInt(vyw430, vyw450)
new_primEqInt(Neg(Zero), Neg(Succ(vyw40000))) → False
new_primEqInt(Neg(Succ(vyw3000)), Neg(Zero)) → False
new_primCompAux0(vyw114, GT) → GT
new_lt20(vyw4311, vyw4511, ty_Integer) → new_lt8(vyw4311, vyw4511)
new_esEs8(EQ, EQ) → True
new_primPlusNat1(Zero, vyw400000) → Succ(vyw400000)
new_esEs23(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Float) → new_esEs13(vyw302, vyw4002)
new_esEs20(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_compare24(vyw430, vyw450, True, ee, ef) → EQ
new_esEs31(vyw30, vyw400, app(app(ty_Either, dag), chd)) → new_esEs5(vyw30, vyw400, dag, chd)
new_esEs25(vyw430, vyw450, app(ty_Ratio, ccf)) → new_esEs19(vyw430, vyw450, ccf)
new_esEs28(vyw4310, vyw4510, app(ty_[], dde)) → new_esEs14(vyw4310, vyw4510, dde)
new_esEs20(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_lt21(vyw4310, vyw4510, app(ty_[], dde)) → new_lt9(vyw4310, vyw4510, dde)
new_lt19(vyw4310, vyw4510, ty_Float) → new_lt11(vyw4310, vyw4510)
new_ltEs11(vyw431, vyw451) → new_not(new_esEs8(new_compare19(vyw431, vyw451), GT))
new_ltEs18(vyw431, vyw451, ty_Ordering) → new_ltEs4(vyw431, vyw451)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_ltEs4(EQ, LT) → False
new_lt16(vyw430, vyw450, ty_@0) → new_lt6(vyw430, vyw450)
new_esEs25(vyw430, vyw450, ty_@0) → new_esEs17(vyw430, vyw450)
new_esEs28(vyw4310, vyw4510, app(app(ty_@2, ddb), ddc)) → new_esEs7(vyw4310, vyw4510, ddb, ddc)
new_esEs29(vyw4311, vyw4511, ty_Float) → new_esEs13(vyw4311, vyw4511)
new_lt5(vyw430, vyw450) → new_esEs8(new_compare8(vyw430, vyw450), LT)
new_primCmpNat0(Succ(vyw43000), Succ(vyw45000)) → new_primCmpNat0(vyw43000, vyw45000)
new_ltEs17(vyw431, vyw451, cdd) → new_not(new_esEs8(new_compare6(vyw431, vyw451, cdd), GT))
new_esEs26(vyw300, vyw4000, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_lt19(vyw4310, vyw4510, ty_Integer) → new_lt8(vyw4310, vyw4510)
new_compare11(vyw430, vyw450, False, eg) → GT
new_esEs6(Nothing, Nothing, bgd) → True
new_primEqInt(Pos(Succ(vyw3000)), Pos(Succ(vyw40000))) → new_primEqNat0(vyw3000, vyw40000)
new_compare10(vyw430, vyw450, False, ee, ef) → GT
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(ty_Either, bdc), bdd), bdb) → new_ltEs5(vyw4310, vyw4510, bdc, bdd)
new_lt19(vyw4310, vyw4510, app(app(ty_@2, cff), cfg)) → new_lt12(vyw4310, vyw4510, cff, cfg)
new_esEs21(vyw301, vyw4001, app(ty_Maybe, hh)) → new_esEs6(vyw301, vyw4001, hh)
new_esEs9(vyw300, vyw4000, app(app(ty_@2, ca), cb)) → new_esEs7(vyw300, vyw4000, ca, cb)
new_esEs30(vyw31, vyw32, vyw33, vyw34, False, bbc, bbd) → new_esEs8(new_compare211(@2(vyw31, vyw32), @2(vyw33, vyw34), False, bbc, bbd), LT)
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(app(ty_Either, dbf), dbg)) → new_esEs5(vyw300, vyw4000, dbf, dbg)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Int) → new_esEs11(vyw300, vyw4000)
new_esEs6(Just(vyw300), Nothing, bgd) → False
new_esEs6(Nothing, Just(vyw4000), bgd) → False
new_primEqNat0(Succ(vyw3000), Succ(vyw40000)) → new_primEqNat0(vyw3000, vyw40000)
new_esEs27(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Integer) → new_ltEs8(vyw4310, vyw4510)
new_esEs21(vyw301, vyw4001, app(ty_[], gg)) → new_esEs14(vyw301, vyw4001, gg)
new_compare31(vyw4300, vyw4500, app(app(ty_@2, cae), caf)) → new_compare28(vyw4300, vyw4500, cae, caf)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Bool) → new_ltEs12(vyw4310, vyw4510)
new_ltEs14(vyw431, vyw451) → new_not(new_esEs8(new_compare15(vyw431, vyw451), GT))
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Int) → new_ltEs16(vyw4310, vyw4510)
new_esEs10(vyw301, vyw4001, ty_Double) → new_esEs15(vyw301, vyw4001)
new_ltEs19(vyw4311, vyw4511, ty_Double) → new_ltEs14(vyw4311, vyw4511)
new_esEs22(vyw302, vyw4002, ty_Bool) → new_esEs12(vyw302, vyw4002)
new_ltEs4(GT, EQ) → False
new_esEs28(vyw4310, vyw4510, ty_Int) → new_esEs11(vyw4310, vyw4510)
new_primCmpInt(Neg(Succ(vyw43000)), Neg(vyw4500)) → new_primCmpNat0(vyw4500, Succ(vyw43000))
new_esEs10(vyw301, vyw4001, app(app(ty_@2, dd), de)) → new_esEs7(vyw301, vyw4001, dd, de)
new_esEs21(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_esEs28(vyw4310, vyw4510, ty_Ordering) → new_esEs8(vyw4310, vyw4510)
new_lt21(vyw4310, vyw4510, ty_Double) → new_lt13(vyw4310, vyw4510)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Zero), Pos(Succ(vyw40000))) → False
new_primEqInt(Pos(Succ(vyw3000)), Pos(Zero)) → False
new_ltEs16(vyw431, vyw451) → new_not(new_esEs8(new_compare8(vyw431, vyw451), GT))
new_ltEs19(vyw4311, vyw4511, app(ty_Maybe, cgg)) → new_ltEs6(vyw4311, vyw4511, cgg)
new_ltEs4(EQ, EQ) → True
new_primPlusNat0(Succ(vyw7700), Zero) → Succ(vyw7700)
new_primPlusNat0(Zero, Succ(vyw4000000)) → Succ(vyw4000000)
new_ltEs18(vyw431, vyw451, ty_Float) → new_ltEs11(vyw431, vyw451)
new_ltEs6(Just(vyw4310), Nothing, cba) → False
new_primCmpNat0(Zero, Zero) → EQ
new_primCmpNat0(Succ(vyw43000), Zero) → GT
new_esEs32(vyw32, vyw34, app(ty_Maybe, bcf)) → new_esEs6(vyw32, vyw34, bcf)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Char, chd) → new_esEs18(vyw300, vyw4000)
new_compare16(vyw430, vyw450, eg) → new_compare25(vyw430, vyw450, new_esEs6(vyw430, vyw450, eg), eg)
new_esEs20(vyw300, vyw4000, app(app(app(ty_@3, fh), ga), gb)) → new_esEs4(vyw300, vyw4000, fh, ga, gb)
new_primCmpInt(Neg(Zero), Pos(Succ(vyw45000))) → LT
new_esEs29(vyw4311, vyw4511, app(app(app(ty_@3, ddf), ddg), ddh)) → new_esEs4(vyw4311, vyw4511, ddf, ddg, ddh)
new_compare9(@0, @0) → EQ
new_esEs20(vyw300, vyw4000, app(app(ty_Either, gc), gd)) → new_esEs5(vyw300, vyw4000, gc, gd)
new_ltEs4(GT, LT) → False
new_esEs28(vyw4310, vyw4510, app(ty_Ratio, ddd)) → new_esEs19(vyw4310, vyw4510, ddd)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Float, chd) → new_esEs13(vyw300, vyw4000)
new_esEs32(vyw32, vyw34, ty_@0) → new_esEs17(vyw32, vyw34)
new_compare14(vyw430, vyw450, False, bfe, bff, bfg) → GT
new_lt21(vyw4310, vyw4510, ty_Integer) → new_lt8(vyw4310, vyw4510)
new_primEqInt(Neg(Succ(vyw3000)), Pos(vyw4000)) → False
new_primEqInt(Pos(Succ(vyw3000)), Neg(vyw4000)) → False
new_esEs10(vyw301, vyw4001, ty_Char) → new_esEs18(vyw301, vyw4001)
new_esEs28(vyw4310, vyw4510, app(app(ty_Either, dcg), dch)) → new_esEs5(vyw4310, vyw4510, dcg, dch)
new_esEs10(vyw301, vyw4001, app(ty_[], dc)) → new_esEs14(vyw301, vyw4001, dc)
new_esEs32(vyw32, vyw34, app(app(ty_Either, bcc), bcd)) → new_esEs5(vyw32, vyw34, bcc, bcd)
new_ltEs19(vyw4311, vyw4511, ty_@0) → new_ltEs15(vyw4311, vyw4511)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Integer) → new_esEs16(vyw300, vyw4000)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Double, bdb) → new_ltEs14(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Maybe, cbg)) → new_ltEs6(vyw4310, vyw4510, cbg)
new_esEs9(vyw300, vyw4000, app(app(ty_Either, cf), cg)) → new_esEs5(vyw300, vyw4000, cf, cg)
new_esEs28(vyw4310, vyw4510, app(ty_Maybe, dda)) → new_esEs6(vyw4310, vyw4510, dda)
new_primEqInt(Neg(Zero), Pos(Succ(vyw40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vyw40000))) → False
new_primCmpInt(Pos(Zero), Pos(Succ(vyw45000))) → new_primCmpNat0(Zero, Succ(vyw45000))
new_esEs31(vyw30, vyw400, ty_Integer) → new_esEs16(vyw30, vyw400)
new_esEs27(vyw4310, vyw4510, app(app(ty_@2, cff), cfg)) → new_esEs7(vyw4310, vyw4510, cff, cfg)
new_lt21(vyw4310, vyw4510, ty_Char) → new_lt17(vyw4310, vyw4510)
new_compare12(vyw430, vyw450, False) → GT
new_lt20(vyw4311, vyw4511, ty_Ordering) → new_lt4(vyw4311, vyw4511)
new_compare31(vyw4300, vyw4500, ty_Ordering) → new_compare5(vyw4300, vyw4500)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Integer) → new_esEs16(vyw300, vyw4000)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_ltEs18(vyw431, vyw451, ty_@0) → new_ltEs15(vyw431, vyw451)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs21(vyw301, vyw4001, ty_Char) → new_esEs18(vyw301, vyw4001)
new_lt16(vyw430, vyw450, app(app(app(ty_@3, bfe), bff), bfg)) → new_lt15(vyw430, vyw450, bfe, bff, bfg)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(app(app(ty_@3, bec), bed), bee)) → new_ltEs10(vyw4310, vyw4510, bec, bed, bee)
new_primCompAux0(vyw114, LT) → LT
new_esEs9(vyw300, vyw4000, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_lt8(vyw430, vyw450) → new_esEs8(new_compare7(vyw430, vyw450), LT)
new_ltEs19(vyw4311, vyw4511, app(app(ty_@2, cgh), cha)) → new_ltEs13(vyw4311, vyw4511, cgh, cha)
new_esEs11(vyw30, vyw400) → new_primEqInt(vyw30, vyw400)
new_not(False) → True
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Int) → new_ltEs16(vyw4310, vyw4510)
new_lt16(vyw430, vyw450, app(app(ty_@2, bga), bgb)) → new_lt12(vyw430, vyw450, bga, bgb)
new_primCmpInt(Pos(Succ(vyw43000)), Pos(vyw4500)) → new_primCmpNat0(Succ(vyw43000), vyw4500)
new_lt16(vyw430, vyw450, ty_Float) → new_lt11(vyw430, vyw450)
new_ltEs15(vyw431, vyw451) → new_not(new_esEs8(new_compare9(vyw431, vyw451), GT))
new_esEs32(vyw32, vyw34, ty_Ordering) → new_esEs8(vyw32, vyw34)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(ty_Either, cbe), cbf)) → new_ltEs5(vyw4310, vyw4510, cbe, cbf)
new_lt20(vyw4311, vyw4511, app(app(app(ty_@3, ddf), ddg), ddh)) → new_lt15(vyw4311, vyw4511, ddf, ddg, ddh)
new_lt14(vyw430, vyw450) → new_esEs8(new_compare29(vyw430, vyw450), LT)
new_compare17(vyw430, vyw450, True) → LT
new_esEs25(vyw430, vyw450, app(app(app(ty_@3, bfe), bff), bfg)) → new_esEs4(vyw430, vyw450, bfe, bff, bfg)
new_esEs9(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_lt20(vyw4311, vyw4511, ty_Double) → new_lt13(vyw4311, vyw4511)
new_compare0(:(vyw4300, vyw4301), [], bfh) → GT
new_compare31(vyw4300, vyw4500, ty_@0) → new_compare9(vyw4300, vyw4500)
new_lt21(vyw4310, vyw4510, ty_Int) → new_lt5(vyw4310, vyw4510)
new_esEs32(vyw32, vyw34, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs4(vyw32, vyw34, bbh, bca, bcb)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(ty_[], bfd)) → new_ltEs7(vyw4310, vyw4510, bfd)
new_esEs22(vyw302, vyw4002, app(app(app(ty_@3, bad), bae), baf)) → new_esEs4(vyw302, vyw4002, bad, bae, baf)
new_esEs26(vyw300, vyw4000, app(app(ty_Either, ced), cee)) → new_esEs5(vyw300, vyw4000, ced, cee)
new_lt19(vyw4310, vyw4510, app(ty_Ratio, cfh)) → new_lt18(vyw4310, vyw4510, cfh)
new_ltEs18(vyw431, vyw451, ty_Bool) → new_ltEs12(vyw431, vyw451)
new_esEs27(vyw4310, vyw4510, ty_Int) → new_esEs11(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Bool) → new_ltEs12(vyw4310, vyw4510)
new_esEs5(Left(vyw300), Left(vyw4000), ty_Double, chd) → new_esEs15(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, ty_Char) → new_esEs18(vyw302, vyw4002)
new_primCmpInt(Pos(Succ(vyw43000)), Neg(vyw4500)) → GT
new_esEs21(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_lt19(vyw4310, vyw4510, ty_Char) → new_lt17(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_primMulInt(Pos(vyw3000), Pos(vyw40000)) → Pos(new_primMulNat0(vyw3000, vyw40000))
new_esEs24(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_esEs10(vyw301, vyw4001, ty_@0) → new_esEs17(vyw301, vyw4001)
new_compare24(vyw430, vyw450, False, ee, ef) → new_compare10(vyw430, vyw450, new_ltEs5(vyw430, vyw450, ee, ef), ee, ef)
new_esEs5(Left(vyw300), Left(vyw4000), ty_@0, chd) → new_esEs17(vyw300, vyw4000)
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(app(app(ty_@3, dbc), dbd), dbe)) → new_esEs4(vyw300, vyw4000, dbc, dbd, dbe)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_[], bge)) → new_esEs14(vyw300, vyw4000, bge)
new_lt20(vyw4311, vyw4511, app(app(ty_Either, dea), deb)) → new_lt10(vyw4311, vyw4511, dea, deb)
new_esEs27(vyw4310, vyw4510, ty_Double) → new_esEs15(vyw4310, vyw4510)
new_esEs15(Double(vyw300, vyw301), Double(vyw4000, vyw4001)) → new_esEs11(new_sr0(vyw300, vyw4000), new_sr0(vyw301, vyw4001))
new_esEs5(Left(vyw300), Right(vyw4000), dag, chd) → False
new_esEs5(Right(vyw300), Left(vyw4000), dag, chd) → False
new_primMulInt(Neg(vyw3000), Neg(vyw40000)) → Pos(new_primMulNat0(vyw3000, vyw40000))
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs10(vyw301, vyw4001, ty_Float) → new_esEs13(vyw301, vyw4001)
new_ltEs19(vyw4311, vyw4511, app(app(ty_Either, cge), cgf)) → new_ltEs5(vyw4311, vyw4511, cge, cgf)
new_primEqNat0(Succ(vyw3000), Zero) → False
new_primEqNat0(Zero, Succ(vyw40000)) → False
new_primPlusNat0(Zero, Zero) → Zero
new_lt20(vyw4311, vyw4511, app(app(ty_@2, ded), dee)) → new_lt12(vyw4311, vyw4511, ded, dee)
new_esEs26(vyw300, vyw4000, app(app(ty_@2, cdg), cdh)) → new_esEs7(vyw300, vyw4000, cdg, cdh)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_Ratio, bhe)) → new_esEs19(vyw300, vyw4000, bhe)
new_esEs25(vyw430, vyw450, app(ty_Maybe, eg)) → new_esEs6(vyw430, vyw450, eg)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Double) → new_ltEs14(vyw4310, vyw4510)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Float, bdb) → new_ltEs11(vyw4310, vyw4510)
new_esEs20(vyw300, vyw4000, app(ty_Ratio, ge)) → new_esEs19(vyw300, vyw4000, ge)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_Ratio, ccb)) → new_ltEs17(vyw4310, vyw4510, ccb)
new_esEs7(@2(vyw300, vyw301), @2(vyw4000, vyw4001), bf, bg) → new_asAs(new_esEs9(vyw300, vyw4000, bf), new_esEs10(vyw301, vyw4001, bg))
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_Maybe, bde), bdb) → new_ltEs6(vyw4310, vyw4510, bde)
new_lt21(vyw4310, vyw4510, ty_Float) → new_lt11(vyw4310, vyw4510)
new_compare210(vyw430, vyw450, True) → EQ
new_esEs6(Just(vyw300), Just(vyw4000), ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs27(vyw4310, vyw4510, ty_Integer) → new_esEs16(vyw4310, vyw4510)
new_esEs23(vyw300, vyw4000, ty_Int) → new_esEs11(vyw300, vyw4000)
new_ltEs4(LT, GT) → True
new_primPlusNat1(Succ(vyw770), vyw400000) → Succ(Succ(new_primPlusNat0(vyw770, vyw400000)))
new_ltEs19(vyw4311, vyw4511, ty_Char) → new_ltEs9(vyw4311, vyw4511)
new_ltEs20(vyw4312, vyw4512, app(ty_Maybe, dfe)) → new_ltEs6(vyw4312, vyw4512, dfe)
new_lt12(vyw430, vyw450, bga, bgb) → new_esEs8(new_compare28(vyw430, vyw450, bga, bgb), LT)
new_lt16(vyw430, vyw450, ty_Double) → new_lt13(vyw430, vyw450)
new_esEs25(vyw430, vyw450, ty_Integer) → new_esEs16(vyw430, vyw450)
new_primCmpInt(Neg(Zero), Neg(Succ(vyw45000))) → new_primCmpNat0(Succ(vyw45000), Zero)
new_primCmpInt(Pos(Zero), Neg(Succ(vyw45000))) → GT
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Int) → new_esEs11(vyw300, vyw4000)
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Int, bdb) → new_ltEs16(vyw4310, vyw4510)
new_esEs32(vyw32, vyw34, ty_Float) → new_esEs13(vyw32, vyw34)
new_compare13(Char(vyw4300), Char(vyw4500)) → new_primCmpNat0(vyw4300, vyw4500)
new_compare0(:(vyw4300, vyw4301), :(vyw4500, vyw4501), bfh) → new_primCompAux1(vyw4300, vyw4500, new_compare0(vyw4301, vyw4501, bfh), bfh)
new_ltEs19(vyw4311, vyw4511, app(ty_[], chc)) → new_ltEs7(vyw4311, vyw4511, chc)
new_esEs32(vyw32, vyw34, ty_Int) → new_esEs11(vyw32, vyw34)
new_esEs27(vyw4310, vyw4510, ty_@0) → new_esEs17(vyw4310, vyw4510)
new_sr0(vyw300, vyw4000) → new_primMulInt(vyw300, vyw4000)
new_lt16(vyw430, vyw450, app(ty_[], bfh)) → new_lt9(vyw430, vyw450, bfh)
new_esEs21(vyw301, vyw4001, app(app(app(ty_@3, hb), hc), hd)) → new_esEs4(vyw301, vyw4001, hb, hc, hd)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(app(ty_@3, bgh), bha), bhb)) → new_esEs4(vyw300, vyw4000, bgh, bha, bhb)
new_lt21(vyw4310, vyw4510, ty_Ordering) → new_lt4(vyw4310, vyw4510)
new_lt16(vyw430, vyw450, app(app(ty_Either, ee), ef)) → new_lt10(vyw430, vyw450, ee, ef)
new_esEs24(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_esEs6(Just(vyw300), Just(vyw4000), app(app(ty_Either, bhc), bhd)) → new_esEs5(vyw300, vyw4000, bhc, bhd)
new_esEs16(Integer(vyw300), Integer(vyw4000)) → new_primEqInt(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, app(app(ty_@2, bfa), bfb)) → new_ltEs13(vyw4310, vyw4510, bfa, bfb)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(ty_@2, chf), chg), chd) → new_esEs7(vyw300, vyw4000, chf, chg)
new_lt16(vyw430, vyw450, ty_Integer) → new_lt8(vyw430, vyw450)
new_esEs21(vyw301, vyw4001, ty_Float) → new_esEs13(vyw301, vyw4001)
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(ty_[], dah)) → new_esEs14(vyw300, vyw4000, dah)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_esEs25(vyw430, vyw450, ty_Bool) → new_esEs12(vyw430, vyw450)
new_ltEs4(LT, EQ) → True
new_primCompAux1(vyw4300, vyw4500, vyw106, bfh) → new_primCompAux0(vyw106, new_compare31(vyw4300, vyw4500, bfh))
new_lt19(vyw4310, vyw4510, ty_Ordering) → new_lt4(vyw4310, vyw4510)
new_esEs20(vyw300, vyw4000, app(ty_Maybe, gf)) → new_esEs6(vyw300, vyw4000, gf)
new_lt19(vyw4310, vyw4510, ty_Bool) → new_lt14(vyw4310, vyw4510)
new_esEs10(vyw301, vyw4001, app(app(ty_Either, ea), eb)) → new_esEs5(vyw301, vyw4001, ea, eb)
new_compare31(vyw4300, vyw4500, app(ty_Maybe, cad)) → new_compare16(vyw4300, vyw4500, cad)
new_lt20(vyw4311, vyw4511, app(ty_Maybe, dec)) → new_lt7(vyw4311, vyw4511, dec)
new_compare26(vyw430, vyw450, False) → new_compare17(vyw430, vyw450, new_ltEs4(vyw430, vyw450))
new_asAs(False, vyw53) → False
new_esEs29(vyw4311, vyw4511, ty_Bool) → new_esEs12(vyw4311, vyw4511)
new_compare18(vyw430, vyw450, ee, ef) → new_compare24(vyw430, vyw450, new_esEs5(vyw430, vyw450, ee, ef), ee, ef)
new_primMulInt(Neg(vyw3000), Pos(vyw40000)) → Neg(new_primMulNat0(vyw3000, vyw40000))
new_primMulInt(Pos(vyw3000), Neg(vyw40000)) → Neg(new_primMulNat0(vyw3000, vyw40000))
new_compare211(@2(vyw430, vyw431), @2(vyw450, vyw451), False, ccd, cce) → new_compare110(vyw430, vyw431, vyw450, vyw451, new_lt16(vyw430, vyw450, ccd), new_asAs(new_esEs25(vyw430, vyw450, ccd), new_ltEs18(vyw431, vyw451, cce)), ccd, cce)
new_primMulNat0(Succ(vyw30000), Zero) → Zero
new_primMulNat0(Zero, Succ(vyw400000)) → Zero
new_esEs9(vyw300, vyw4000, ty_@0) → new_esEs17(vyw300, vyw4000)
new_esEs21(vyw301, vyw4001, app(app(ty_Either, he), hf)) → new_esEs5(vyw301, vyw4001, he, hf)
new_esEs6(Just(vyw300), Just(vyw4000), app(ty_Maybe, bhf)) → new_esEs6(vyw300, vyw4000, bhf)
new_esEs21(vyw301, vyw4001, ty_Ordering) → new_esEs8(vyw301, vyw4001)
new_esEs29(vyw4311, vyw4511, ty_Int) → new_esEs11(vyw4311, vyw4511)
new_esEs9(vyw300, vyw4000, ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs10(vyw301, vyw4001, app(ty_Maybe, ed)) → new_esEs6(vyw301, vyw4001, ed)
new_compare15(Double(vyw4300, vyw4301), Double(vyw4500, vyw4501)) → new_compare8(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_compare12(vyw430, vyw450, True) → LT
new_compare31(vyw4300, vyw4500, ty_Float) → new_compare19(vyw4300, vyw4500)
new_ltEs12(True, True) → True
new_compare31(vyw4300, vyw4500, app(ty_[], cah)) → new_compare0(vyw4300, vyw4500, cah)
new_ltEs18(vyw431, vyw451, app(ty_Ratio, cdd)) → new_ltEs17(vyw431, vyw451, cdd)
new_esEs5(Right(vyw300), Right(vyw4000), dag, ty_Double) → new_esEs15(vyw300, vyw4000)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Float) → new_ltEs11(vyw4310, vyw4510)
new_esEs28(vyw4310, vyw4510, ty_Float) → new_esEs13(vyw4310, vyw4510)
new_ltEs6(Just(vyw4310), Just(vyw4510), app(app(app(ty_@3, cbb), cbc), cbd)) → new_ltEs10(vyw4310, vyw4510, cbb, cbc, cbd)
new_ltEs12(False, True) → True
new_lt13(vyw430, vyw450) → new_esEs8(new_compare15(vyw430, vyw450), LT)
new_compare111(vyw86, vyw87, vyw88, vyw89, False, dcb, dcc) → GT
new_esEs10(vyw301, vyw4001, ty_Int) → new_esEs11(vyw301, vyw4001)
new_ltEs18(vyw431, vyw451, app(app(ty_@2, cdb), cdc)) → new_ltEs13(vyw431, vyw451, cdb, cdc)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Integer) → new_ltEs8(vyw4310, vyw4510)
new_lt20(vyw4311, vyw4511, app(ty_Ratio, def)) → new_lt18(vyw4311, vyw4511, def)
new_ltEs19(vyw4311, vyw4511, ty_Int) → new_ltEs16(vyw4311, vyw4511)
new_esEs12(True, False) → False
new_esEs12(False, True) → False
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(ty_Maybe, dca)) → new_esEs6(vyw300, vyw4000, dca)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(app(app(ty_@3, bcg), bch), bda), bdb) → new_ltEs10(vyw4310, vyw4510, bcg, bch, bda)
new_compare211(vyw43, vyw45, True, ccd, cce) → EQ
new_ltEs6(Nothing, Nothing, cba) → True
new_esEs27(vyw4310, vyw4510, ty_Bool) → new_esEs12(vyw4310, vyw4510)
new_esEs29(vyw4311, vyw4511, ty_Double) → new_esEs15(vyw4311, vyw4511)
new_ltEs5(Left(vyw4310), Left(vyw4510), app(ty_[], bea), bdb) → new_ltEs7(vyw4310, vyw4510, bea)
new_compare6(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Integer) → new_compare7(new_sr(vyw4300, vyw4501), new_sr(vyw4500, vyw4301))
new_ltEs6(Just(vyw4310), Just(vyw4510), app(ty_[], ccc)) → new_ltEs7(vyw4310, vyw4510, ccc)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_@0) → new_ltEs15(vyw4310, vyw4510)
new_ltEs4(LT, LT) → True
new_compare19(Float(vyw4300, vyw4301), Float(vyw4500, vyw4501)) → new_compare8(new_sr0(vyw4300, vyw4500), new_sr0(vyw4301, vyw4501))
new_ltEs20(vyw4312, vyw4512, ty_Float) → new_ltEs11(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, app(app(ty_Either, dcg), dch)) → new_lt10(vyw4310, vyw4510, dcg, dch)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_Ordering) → new_ltEs4(vyw4310, vyw4510)
new_lt10(vyw430, vyw450, ee, ef) → new_esEs8(new_compare18(vyw430, vyw450, ee, ef), LT)
new_esEs31(vyw30, vyw400, ty_Float) → new_esEs13(vyw30, vyw400)
new_ltEs18(vyw431, vyw451, ty_Double) → new_ltEs14(vyw431, vyw451)
new_lt20(vyw4311, vyw4511, ty_Float) → new_lt11(vyw4311, vyw4511)
new_compare7(Integer(vyw4300), Integer(vyw4500)) → new_primCmpInt(vyw4300, vyw4500)
new_esEs10(vyw301, vyw4001, ty_Integer) → new_esEs16(vyw301, vyw4001)
new_esEs5(Left(vyw300), Left(vyw4000), app(app(ty_Either, dac), dad), chd) → new_esEs5(vyw300, vyw4000, dac, dad)
new_ltEs18(vyw431, vyw451, app(ty_Maybe, cba)) → new_ltEs6(vyw431, vyw451, cba)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Ordering) → new_esEs8(vyw300, vyw4000)
new_esEs31(vyw30, vyw400, ty_Char) → new_esEs18(vyw30, vyw400)
new_esEs22(vyw302, vyw4002, ty_Integer) → new_esEs16(vyw302, vyw4002)
new_ltEs20(vyw4312, vyw4512, ty_Integer) → new_ltEs8(vyw4312, vyw4512)
new_lt21(vyw4310, vyw4510, app(app(app(ty_@3, dcd), dce), dcf)) → new_lt15(vyw4310, vyw4510, dcd, dce, dcf)
new_esEs26(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_esEs29(vyw4311, vyw4511, ty_Integer) → new_esEs16(vyw4311, vyw4511)
new_esEs20(vyw300, vyw4000, app(app(ty_@2, ff), fg)) → new_esEs7(vyw300, vyw4000, ff, fg)
new_compare210(vyw430, vyw450, False) → new_compare12(vyw430, vyw450, new_ltEs12(vyw430, vyw450))
new_esEs10(vyw301, vyw4001, ty_Ordering) → new_esEs8(vyw301, vyw4001)
new_esEs5(Right(vyw300), Right(vyw4000), dag, app(app(ty_@2, dba), dbb)) → new_esEs7(vyw300, vyw4000, dba, dbb)
new_lt21(vyw4310, vyw4510, ty_@0) → new_lt6(vyw4310, vyw4510)
new_primPlusNat0(Succ(vyw7700), Succ(vyw4000000)) → Succ(Succ(new_primPlusNat0(vyw7700, vyw4000000)))
new_ltEs5(Left(vyw4310), Left(vyw4510), ty_Char, bdb) → new_ltEs9(vyw4310, vyw4510)
new_lt19(vyw4310, vyw4510, ty_@0) → new_lt6(vyw4310, vyw4510)
new_ltEs5(Right(vyw4310), Right(vyw4510), beb, ty_@0) → new_ltEs15(vyw4310, vyw4510)
new_compare0([], :(vyw4500, vyw4501), bfh) → LT
new_esEs27(vyw4310, vyw4510, app(ty_[], cga)) → new_esEs14(vyw4310, vyw4510, cga)
new_esEs9(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs14(:(vyw300, vyw301), :(vyw4000, vyw4001), cde) → new_asAs(new_esEs26(vyw300, vyw4000, cde), new_esEs14(vyw301, vyw4001, cde))
new_compare31(vyw4300, vyw4500, ty_Char) → new_compare13(vyw4300, vyw4500)
new_asAs(True, vyw53) → vyw53
new_esEs25(vyw430, vyw450, ty_Int) → new_esEs11(vyw430, vyw450)
new_esEs20(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs26(vyw300, vyw4000, ty_Double) → new_esEs15(vyw300, vyw4000)
new_esEs31(vyw30, vyw400, ty_Bool) → new_esEs12(vyw30, vyw400)
new_ltEs6(Just(vyw4310), Just(vyw4510), ty_Ordering) → new_ltEs4(vyw4310, vyw4510)
new_compare17(vyw430, vyw450, False) → GT
new_compare27(vyw430, vyw450, True, bfe, bff, bfg) → EQ
new_esEs31(vyw30, vyw400, ty_Int) → new_esEs11(vyw30, vyw400)
new_ltEs20(vyw4312, vyw4512, app(app(app(ty_@3, deh), dfa), dfb)) → new_ltEs10(vyw4312, vyw4512, deh, dfa, dfb)
new_esEs20(vyw300, vyw4000, app(ty_[], fd)) → new_esEs14(vyw300, vyw4000, fd)
new_esEs9(vyw300, vyw4000, ty_Char) → new_esEs18(vyw300, vyw4000)
new_ltEs20(vyw4312, vyw4512, app(app(ty_@2, dff), dfg)) → new_ltEs13(vyw4312, vyw4512, dff, dfg)
new_ltEs7(vyw431, vyw451, eh) → new_not(new_esEs8(new_compare0(vyw431, vyw451, eh), GT))
new_ltEs19(vyw4311, vyw4511, app(app(app(ty_@3, cgb), cgc), cgd)) → new_ltEs10(vyw4311, vyw4511, cgb, cgc, cgd)
new_esEs27(vyw4310, vyw4510, ty_Char) → new_esEs18(vyw4310, vyw4510)
new_esEs26(vyw300, vyw4000, app(ty_Ratio, cef)) → new_esEs19(vyw300, vyw4000, cef)
new_ltEs4(GT, GT) → True
new_compare30(vyw430, vyw450, bfe, bff, bfg) → new_compare27(vyw430, vyw450, new_esEs4(vyw430, vyw450, bfe, bff, bfg), bfe, bff, bfg)
new_esEs28(vyw4310, vyw4510, ty_Char) → new_esEs18(vyw4310, vyw4510)
new_compare25(vyw430, vyw450, False, eg) → new_compare11(vyw430, vyw450, new_ltEs6(vyw430, vyw450, eg), eg)
new_esEs21(vyw301, vyw4001, ty_Bool) → new_esEs12(vyw301, vyw4001)
new_esEs6(Just(vyw300), Just(vyw4000), ty_Bool) → new_esEs12(vyw300, vyw4000)
new_esEs22(vyw302, vyw4002, app(app(ty_Either, bag), bah)) → new_esEs5(vyw302, vyw4002, bag, bah)
new_esEs31(vyw30, vyw400, app(ty_Maybe, bgd)) → new_esEs6(vyw30, vyw400, bgd)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_primCompAux0(vyw114, EQ) → vyw114
new_esEs29(vyw4311, vyw4511, ty_Ordering) → new_esEs8(vyw4311, vyw4511)
new_ltEs20(vyw4312, vyw4512, app(app(ty_Either, dfc), dfd)) → new_ltEs5(vyw4312, vyw4512, dfc, dfd)
new_ltEs18(vyw431, vyw451, ty_Integer) → new_ltEs8(vyw431, vyw451)
new_esEs32(vyw32, vyw34, ty_Char) → new_esEs18(vyw32, vyw34)
new_esEs28(vyw4310, vyw4510, ty_Bool) → new_esEs12(vyw4310, vyw4510)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs31(vyw30, vyw400, app(app(ty_@2, bf), bg)) → new_esEs7(vyw30, vyw400, bf, bg)
new_primCmpInt(Neg(Succ(vyw43000)), Pos(vyw4500)) → LT
new_compare6(:%(vyw4300, vyw4301), :%(vyw4500, vyw4501), ty_Int) → new_compare8(new_sr0(vyw4300, vyw4501), new_sr0(vyw4500, vyw4301))
new_not(True) → False

The set Q consists of the following terms:

new_lt20(x0, x1, app(ty_Ratio, x2))
new_compare15(Double(x0, x1), Double(x2, x3))
new_lt19(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare111(x0, x1, x2, x3, False, x4, x5)
new_sr0(x0, x1)
new_lt16(x0, x1, app(app(ty_@2, x2), x3))
new_esEs31(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_ltEs20(x0, x1, ty_Float)
new_lt20(x0, x1, ty_Double)
new_esEs28(x0, x1, ty_Ordering)
new_compare31(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs18(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Zero)
new_esEs12(False, False)
new_esEs11(x0, x1)
new_esEs28(x0, x1, ty_Double)
new_compare10(x0, x1, True, x2, x3)
new_esEs22(x0, x1, ty_Ordering)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs20(x0, x1, ty_Double)
new_lt19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_lt21(x0, x1, ty_Ordering)
new_lt19(x0, x1, app(app(ty_@2, x2), x3))
new_compare24(x0, x1, False, x2, x3)
new_compare31(x0, x1, ty_Float)
new_esEs32(x0, x1, ty_Int)
new_ltEs19(x0, x1, ty_Char)
new_compare12(x0, x1, False)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_lt19(x0, x1, ty_Ordering)
new_esEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, ty_Char)
new_compare110(x0, x1, x2, x3, False, x4, x5, x6)
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_esEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare27(x0, x1, True, x2, x3, x4)
new_lt12(x0, x1, x2, x3)
new_esEs16(Integer(x0), Integer(x1))
new_esEs26(x0, x1, ty_Double)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs5(Right(x0), Right(x1), x2, ty_Char)
new_esEs32(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs31(x0, x1, ty_Int)
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_lt16(x0, x1, app(ty_[], x2))
new_ltEs5(Right(x0), Right(x1), x2, ty_Bool)
new_lt20(x0, x1, app(ty_[], x2))
new_lt16(x0, x1, ty_Float)
new_esEs8(GT, GT)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_asAs(True, x0)
new_ltEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Left(x0), Left(x1), ty_Char, x2)
new_lt21(x0, x1, ty_Integer)
new_esEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs26(x0, x1, ty_Float)
new_esEs8(LT, LT)
new_ltEs20(x0, x1, ty_Integer)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_Ordering)
new_ltEs8(x0, x1)
new_ltEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs29(x0, x1, ty_Float)
new_esEs31(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Char)
new_lt13(x0, x1)
new_esEs5(Right(x0), Right(x1), x2, ty_Integer)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Char)
new_ltEs5(Right(x0), Right(x1), x2, ty_@0)
new_compare25(x0, x1, False, x2)
new_compare30(x0, x1, x2, x3, x4)
new_compare28(x0, x1, x2, x3)
new_esEs10(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Int)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs10(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs5(Left(x0), Left(x1), ty_Char, x2)
new_compare17(x0, x1, False)
new_ltEs5(Right(x0), Right(x1), x2, ty_Float)
new_ltEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_ltEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primCompAux0(x0, EQ)
new_esEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_compare26(x0, x1, True)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Double)
new_esEs29(x0, x1, ty_Char)
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_lt16(x0, x1, app(ty_Ratio, x2))
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_lt21(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_lt6(x0, x1)
new_lt20(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Int)
new_ltEs18(x0, x1, ty_Integer)
new_esEs29(x0, x1, ty_Integer)
new_lt21(x0, x1, app(ty_[], x2))
new_compare0(:(x0, x1), :(x2, x3), x4)
new_primEqNat0(Succ(x0), Zero)
new_compare31(x0, x1, ty_Integer)
new_compare6(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs9(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs31(x0, x1, app(ty_Ratio, x2))
new_esEs31(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_compare10(x0, x1, False, x2, x3)
new_primPlusNat1(Succ(x0), x1)
new_esEs32(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_Int)
new_esEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_compare13(Char(x0), Char(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Zero, Zero)
new_ltEs18(x0, x1, app(ty_[], x2))
new_primCompAux1(x0, x1, x2, x3)
new_ltEs5(Left(x0), Right(x1), x2, x3)
new_ltEs5(Right(x0), Left(x1), x2, x3)
new_esEs32(x0, x1, app(ty_Ratio, x2))
new_sr(Integer(x0), Integer(x1))
new_esEs14(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Int)
new_esEs28(x0, x1, app(ty_[], x2))
new_compare16(x0, x1, x2)
new_lt19(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_compare25(x0, x1, True, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_ltEs4(GT, GT)
new_esEs28(x0, x1, ty_@0)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_lt19(x0, x1, ty_Int)
new_esEs31(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs32(x0, x1, ty_Integer)
new_lt16(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs10(x0, x1, ty_Integer)
new_esEs10(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_ltEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs28(x0, x1, ty_Bool)
new_ltEs20(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs31(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs5(Left(x0), Left(x1), ty_Integer, x2)
new_primEqNat0(Zero, Succ(x0))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, ty_@0)
new_compare31(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, ty_Integer)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs16(x0, x1)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs5(Left(x0), Left(x1), ty_Bool, x2)
new_ltEs12(False, False)
new_esEs31(x0, x1, ty_Char)
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Integer)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_compare26(x0, x1, False)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_lt21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs32(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_ltEs19(x0, x1, ty_Int)
new_esEs29(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Bool)
new_esEs29(x0, x1, ty_Double)
new_compare14(x0, x1, True, x2, x3, x4)
new_compare31(x0, x1, ty_Int)
new_esEs5(Right(x0), Right(x1), x2, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs28(x0, x1, ty_Float)
new_esEs32(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Ordering)
new_lt19(x0, x1, ty_Integer)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, x0)
new_esEs31(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Bool)
new_esEs9(x0, x1, ty_Float)
new_primPlusNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Bool)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_lt16(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_ltEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1)
new_esEs5(Left(x0), Left(x1), ty_Double, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs28(x0, x1, ty_Char)
new_ltEs18(x0, x1, app(ty_Ratio, x2))
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_compare31(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_[], x2))
new_primCmpInt(Neg(Zero), Neg(Zero))
new_primCompAux0(x0, LT)
new_compare31(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs4(EQ, EQ)
new_lt21(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs21(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_ltEs19(x0, x1, ty_Double)
new_esEs17(@0, @0)
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs5(Right(x0), Right(x1), x2, ty_Integer)
new_ltEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, ty_Ordering)
new_esEs4(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_compare31(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_compare210(x0, x1, False)
new_compare0([], :(x0, x1), x2)
new_esEs28(x0, x1, ty_Integer)
new_compare14(x0, x1, False, x2, x3, x4)
new_ltEs4(LT, EQ)
new_ltEs4(EQ, LT)
new_compare29(x0, x1)
new_esEs21(x0, x1, ty_Bool)
new_compare211(x0, x1, True, x2, x3)
new_compare110(x0, x1, x2, x3, True, x4, x5, x6)
new_esEs6(Nothing, Nothing, x0)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_Float)
new_compare0([], [], x0)
new_ltEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs12(True, True)
new_lt16(x0, x1, app(app(ty_Either, x2), x3))
new_esEs29(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, app(ty_[], x2))
new_esEs29(x0, x1, app(app(ty_Either, x2), x3))
new_lt16(x0, x1, ty_@0)
new_compare31(x0, x1, app(app(ty_Either, x2), x3))
new_pePe(True, x0)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_@0)
new_ltEs18(x0, x1, ty_Float)
new_ltEs5(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Integer)
new_ltEs5(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_lt20(x0, x1, ty_Bool)
new_ltEs20(x0, x1, ty_Char)
new_ltEs19(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_pePe(False, x0)
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_lt21(x0, x1, ty_Double)
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_ltEs18(x0, x1, ty_Double)
new_lt7(x0, x1, x2)
new_compare12(x0, x1, True)
new_lt20(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_lt20(x0, x1, ty_Ordering)
new_esEs32(x0, x1, ty_Ordering)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs8(EQ, EQ)
new_primCmpNat0(Zero, Succ(x0))
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1)
new_esEs24(x0, x1, ty_Integer)
new_esEs32(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_lt8(x0, x1)
new_asAs(False, x0)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_ltEs5(Left(x0), Left(x1), ty_@0, x2)
new_lt19(x0, x1, app(ty_Ratio, x2))
new_ltEs7(x0, x1, x2)
new_ltEs4(LT, LT)
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs27(x0, x1, ty_Double)
new_lt16(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Double)
new_ltEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs27(x0, x1, ty_Float)
new_lt19(x0, x1, ty_Double)
new_esEs6(Just(x0), Nothing, x1)
new_esEs22(x0, x1, ty_Integer)
new_lt19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_primCmpNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs14([], [], x0)
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs31(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Char)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_lt14(x0, x1)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_ltEs14(x0, x1)
new_compare31(x0, x1, ty_Ordering)
new_ltEs5(Right(x0), Right(x1), x2, ty_Int)
new_ltEs19(x0, x1, ty_Bool)
new_ltEs20(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs29(x0, x1, app(ty_[], x2))
new_ltEs12(False, True)
new_ltEs12(True, False)
new_esEs25(x0, x1, ty_Int)
new_esEs31(x0, x1, ty_Double)
new_lt15(x0, x1, x2, x3, x4)
new_esEs29(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_compare0(:(x0, x1), [], x2)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_compare31(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_primCmpNat0(Zero, Zero)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_ltEs6(Nothing, Just(x0), x1)
new_compare111(x0, x1, x2, x3, True, x4, x5)
new_lt21(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_lt18(x0, x1, x2)
new_esEs22(x0, x1, ty_Float)
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_lt16(x0, x1, ty_Char)
new_ltEs18(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(x0, x1, ty_Bool)
new_compare11(x0, x1, True, x2)
new_esEs5(Left(x0), Left(x1), ty_Float, x2)
new_lt16(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs29(x0, x1, ty_@0)
new_compare17(x0, x1, True)
new_lt19(x0, x1, ty_Char)
new_compare210(x0, x1, True)
new_ltEs9(x0, x1)
new_esEs26(x0, x1, app(ty_[], x2))
new_primMulInt(Neg(x0), Neg(x1))
new_esEs30(x0, x1, x2, x3, True, x4, x5)
new_esEs31(x0, x1, ty_@0)
new_ltEs15(x0, x1)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_compare24(x0, x1, True, x2, x3)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs29(x0, x1, ty_Ordering)
new_esEs29(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Char)
new_esEs5(Right(x0), Right(x1), x2, ty_Char)
new_lt19(x0, x1, ty_Float)
new_esEs5(Right(x0), Right(x1), x2, ty_Bool)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs11(x0, x1)
new_esEs32(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_compare9(@0, @0)
new_ltEs6(Just(x0), Nothing, x1)
new_compare211(@2(x0, x1), @2(x2, x3), False, x4, x5)
new_esEs29(x0, x1, ty_Bool)
new_esEs15(Double(x0, x1), Double(x2, x3))
new_esEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs5(Right(x0), Right(x1), x2, ty_@0)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Float)
new_esEs5(Right(x0), Right(x1), x2, ty_Int)
new_esEs20(x0, x1, ty_Ordering)
new_lt4(x0, x1)
new_ltEs4(EQ, GT)
new_ltEs4(GT, EQ)
new_ltEs17(x0, x1, x2)
new_not(True)
new_esEs30(x0, x1, x2, x3, False, x4, x5)
new_lt10(x0, x1, x2, x3)
new_esEs18(Char(x0), Char(x1))
new_compare11(x0, x1, False, x2)
new_ltEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_lt16(x0, x1, ty_Ordering)
new_esEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_primMulInt(Pos(x0), Pos(x1))
new_esEs28(x0, x1, ty_Int)
new_not(False)
new_ltEs18(x0, x1, ty_Char)
new_primCmpNat0(Succ(x0), Succ(x1))
new_ltEs18(x0, x1, ty_@0)
new_compare31(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs12(True, True)
new_ltEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs32(x0, x1, ty_Char)
new_compare5(x0, x1)
new_lt9(x0, x1, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare19(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_@0)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs31(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs29(x0, x1, ty_Int)
new_esEs14([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs9(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_Char)
new_esEs10(x0, x1, ty_Double)
new_esEs32(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_esEs26(x0, x1, ty_Int)
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_esEs31(x0, x1, app(ty_[], x2))
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), ty_Double, x2)
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_lt20(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, ty_Ordering)
new_ltEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Right(x0), Left(x1), x2, x3)
new_esEs5(Left(x0), Right(x1), x2, x3)
new_ltEs20(x0, x1, ty_Bool)
new_lt21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_compare31(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Succ(x1))
new_lt17(x0, x1)
new_primCompAux0(x0, GT)
new_esEs20(x0, x1, ty_Bool)
new_compare31(x0, x1, ty_Bool)
new_compare6(:%(x0, x1), :%(x2, x3), ty_Int)
new_lt19(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs9(x0, x1, ty_Bool)
new_esEs32(x0, x1, app(ty_[], x2))
new_esEs5(Left(x0), Left(x1), ty_Integer, x2)
new_ltEs20(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, ty_@0)
new_esEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_compare7(Integer(x0), Integer(x1))
new_esEs5(Left(x0), Left(x1), ty_@0, x2)
new_lt16(x0, x1, ty_Double)
new_lt21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_@0)
new_lt21(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_lt21(x0, x1, ty_@0)
new_esEs32(x0, x1, ty_Float)
new_ltEs4(LT, GT)
new_ltEs4(GT, LT)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Ordering)
new_primPlusNat0(Zero, Succ(x0))
new_lt11(x0, x1)
new_esEs5(Left(x0), Left(x1), ty_Int, x2)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs25(x0, x1, ty_Double)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_lt21(x0, x1, ty_Float)
new_compare18(x0, x1, x2, x3)
new_compare27(x0, x1, False, x2, x3, x4)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_lt16(x0, x1, ty_Bool)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: